Searched refs:getSmtEngine (Results 1 – 15 of 15) sorted by relevance
56 SmtEngine* getSmtEngine() { return &d_smt; } in getSmtEngine() function58 const SmtEngine* getSmtEngine() const { return &d_smt; } in getSmtEngine() function
55 SmtEngine* getSmtEngine() const { return d_smt; } in getSmtEngine() function
68 Expr normalized = solver->getSmtEngine()->simplify(assert->getExpr()); in main()
90 assertions.push_back(solver->getSmtEngine()->simplify(assert->getExpr())); in main()
93 assertions.push_back(solver->getSmtEngine()->simplify(assert->getExpr())); in main()
72 SmtEngine* getSmtEngine() { return d_smtEngine; } in getSmtEngine() function
70 d_smts.push_back(d_solver->getSmtEngine()); in CommandExecutorPortfolio()78 d_smts.push_back(solver->getSmtEngine()); in CommandExecutorPortfolio()
54 d_smtEngine(d_solver->getSmtEngine()), in CommandExecutor()
274 pExecutor->getSmtEngine()->setFilename(filenameStr); in runCvc4()
72 c->invoke(solver->getSmtEngine(), ss); in testGetInfo()
75 SmtEngine * smt = core.getSmtEngine(); in toStream()
2496 SmtEngine* getSmtEngine(void) const;
3512 SmtEngine* Solver::getSmtEngine(void) const { return d_smtEngine.get(); } in getSmtEngine() function in CVC4::api::Solver
1277 SmtEngine * smt = core.getSmtEngine(); in toStream()1397 Node::fromExpr(theory_model->getSmtEngine()->getValue(n.toExpr())); in toStream()
1142 Node val = Node::fromExpr(model.getSmtEngine()->getValue(n.toExpr())); in DeclareFunctionCommandToStream()