ApproxMC for SMT Solvers. Authors: Supratik Chakraborty, Kuldeep S Meel, Rakesh Mistry, Moshe Y Vardi
-
src/expr/command.cpp (line 999)
Added function:
Expr GetModelCommand::getModelCommandInvoke(SmtEngine* smtEngine, std::ostream& out) throw()
-
src/expr/command.h (line 568)
Added function:
Expr getModelCommandInvoke(SmtEngine* smtEngine, std::ostream& out) throw();
-
src/main/command_executor.cpp (line 149)
Added function:
bool CommandExecutor::doCheckSatCommandSingleton(Command* cmd)
-
src/main/command_executor.h (line 81)
Added function:
bool CommandExecutor::doCheckSatCommandSingleton(Command* cmd);
-
src/main/driver_unified.cpp (lines 423 to 456)
Added model counting code -
src/main/options (line 61)
Added command line optionmaxsolutions
-
src/smt/smt_engine.cpp
Commented lines 1057 to 1065 to enable incremental in eager mode -
src/theory/bv/options_handlers.h
Commented lines 87 to 91 to enable incremental in eager mode -
src/theory/bv/theory_bv.cpp
Commented line 194 to enable incremental in eager mode
To be updated ...