Searched refs:smtEngine (Results 1 – 9 of 9) sorted by relevance
190 invoke(smtEngine); in invoke()333 smtEngine->push(); in invoke()363 smtEngine->pop(); in invoke()924 smtEngine->reset(); in invoke()950 smtEngine->resetAssertions(); in invoke()1361 smtEngine->addToAssignment( in invoke()1826 d_smtEngine = smtEngine; in invoke()1889 d_smtEngine = smtEngine; in invoke()1949 d_smtEngine = smtEngine; in invoke()2002 d_smtEngine = smtEngine; in invoke()[all …]
295 void invoke(SmtEngine* smtEngine) override;312 void invoke(SmtEngine* smtEngine) override;334 void invoke(SmtEngine* smtEngine) override;344 void invoke(SmtEngine* smtEngine) override;354 void invoke(SmtEngine* smtEngine) override;389 void invoke(SmtEngine* smtEngine) override;408 void invoke(SmtEngine* smtEngine) override;430 void invoke(SmtEngine* smtEngine) override;455 void invoke(SmtEngine* smtEngine) override;474 void invoke(SmtEngine* smtEngine) override;[all …]
84 SmtEngine* smtEngine; member in VariableGenerator92 smtEngine->push(); in push()102 smtEngine->pop(); in pop()113 smtEngine->pop(); in clearAssertions()116 smtEngine->pop(); // get back to original clean context in clearAssertions()117 smtEngine->push(); // make a new context so we don't pollute the context we want to pop back to in clearAssertions()
62 smtEngine = new SmtEngine(exprManager); in VariableGenerator()63 smtEngine->setOption("rewrite-divk", SExpr(true)); in VariableGenerator()64 smtEngine->push(); // make a new context so we have a clean context to pop() back to in VariableGenerator()75 delete smtEngine; in ~VariableGenerator()106 smtEngine->assertFormula(e); in assertDag()111 const CVC4::Result result = smtEngine->checkSat(exprManager->mkConst(true)); in assertDag()134 const CVC4::Result result = smtEngine->checkSat(e); in checkDag()
219 exprManager and smtEngine220 (~VariableGenerator): added to destruct exprManger and smtEngine223 (assertDag, checkDag): deref smtEngine226 options; made exprManager and smtEngine into pointers; added decl259 * variableGenerator.cc (VariableGenerator): init smtEngine266 (SMT_VariableManager): added data member smtEngine
344 * SMT_RewriteSearchState.hh (S): deleted data member smtEngine349 (SMT_RewriteSearchState): don't init smtEngine350 (~SMT_RewriteSearchState): don't delete smtEngine
326 LFSCProof(SmtEngine* smtEngine,
546 LFSCProof::LFSCProof(SmtEngine* smtEngine, in LFSCProof() argument553 d_smtEngine(smtEngine) in LFSCProof()
452 …help = "the resource limit is hard potentially leaving the smtEngine in an unsafe state (sho…