diff --git a/src/api/MainSolver.cc b/src/api/MainSolver.cc index 7e8abbd2b..6bec2c254 100644 --- a/src/api/MainSolver.cc +++ b/src/api/MainSolver.cc @@ -24,7 +24,7 @@ namespace opensmt { bool stop; } -MainSolver::MainSolver(Logic& logic, SMTConfig& conf, std::string name) +MainSolver::MainSolver(Logic & logic, SMTConfig & conf, std::string name) : theory(createTheory(logic, conf)), term_mapper(new TermMapper(logic)), @@ -103,10 +103,6 @@ bool MainSolver::pop() return false; } -PartitionManager & MainSolver::getPartitionManager() { return pmanager; } - -sstat MainSolver::getStatus() const { return status; } - void MainSolver::insertFormula(PTRef fla) { if (logic.getSortRef(fla) != logic.getSort_bool()) { @@ -214,6 +210,7 @@ PTRef MainSolver::rewriteMaxArity(PTRef root) } std::unique_ptr MainSolver::getModel() { + if (!config.produce_models()) { throw OsmtApiException("Producing models is not enabled"); } if (status != s_True) { throw OsmtApiException("Model cannot be created if solver is not in SAT state"); } ModelBuilder modelBuilder {logic}; @@ -242,6 +239,7 @@ lbool MainSolver::getTermValue(PTRef tr) const { } std::unique_ptr MainSolver::getInterpolationContext() { + if (!config.produce_inter()) { throw OsmtApiException("Producing interpolants is not enabled"); } if (status != s_False) { throw OsmtApiException("Interpolation context cannot be created if solver is not in UNSAT state"); } return std::make_unique( config, *theory, *term_mapper, getSMTSolver().getResolutionProof(), pmanager diff --git a/src/api/MainSolver.h b/src/api/MainSolver.h index c93ee47b8..a7a88e7e6 100644 --- a/src/api/MainSolver.h +++ b/src/api/MainSolver.h @@ -22,8 +22,7 @@ class Logic; class sstat { - char value; - public: +public: explicit sstat(int v) : value(v) {} bool operator == (sstat s) const { return value == s.value; } bool operator != (sstat s) const { return value != s.value; } @@ -39,6 +38,8 @@ class sstat { } char getValue() const { return value; } friend sstat toSstat(int v); +private: + char value; }; inline sstat toSstat(int v) {return sstat(v); } @@ -50,31 +51,76 @@ const sstat s_Error = toSstat( 2); class MainSolver { -protected: /** Helper classes to deal with assertion stack, preprocessing and substitutions **/ +public: + MainSolver(Logic & logic, SMTConfig & conf, std::string name); + + MainSolver(std::unique_ptr th, std::unique_ptr tm, std::unique_ptr thd, + std::unique_ptr ss, Logic & logic, SMTConfig & conf, std::string name); + + virtual ~MainSolver() = default; + MainSolver (const MainSolver&) = delete; + MainSolver& operator = (const MainSolver&) = delete; + MainSolver (MainSolver&&) = default; + MainSolver& operator = (MainSolver&&) = delete; + + SMTConfig & getConfig() const { return config; } + Logic & getLogic() const { return logic; } + + SimpSMTSolver & getSMTSolver() { return *smt_solver; } + SimpSMTSolver const & getSMTSolver() const { return *smt_solver; } + + THandler & getTHandler() { return *thandler; } + THandler const & getTHandler() const { return *thandler; } + + void push(); + bool pop(); + void insertFormula(PTRef fla); + + void initialize(); + + virtual sstat check(); // A wrapper for solve which simplifies the loaded formulas and initializes the solvers + sstat solve(); + // Simplify frames (not yet simplified) until all are simplified or the instance is detected unsatisfiable. + sstat simplifyFormulas(); + + void printFramesAsQuery() const; + [[nodiscard]] sstat getStatus() const { return status; } + + // Values + lbool getTermValue (PTRef tr) const; + + // Returns model of the last query (must be in satisfiable state) + std::unique_ptr getModel(); + + // Prints proof of the last query (must be in unsatisfiable state) + void printResolutionProofSMT2() const; + + // Returns interpolation context for the last query (must be in UNSAT state) + std::unique_ptr getInterpolationContext(); + + void stop() { smt_solver->stop = true; } + + static std::unique_ptr createTheory(Logic & logic, SMTConfig & config); +protected: using FrameId = uint32_t; struct PushFrame { - private: - FrameId id; - public: FrameId getId() const { return id; } int size() const { return formulas.size(); } void push(PTRef tr) { formulas.push(tr); } PTRef operator[](int i) const { return formulas[i]; } vec formulas; - bool unsat; // If true then the stack of frames with this frame at top is UNSAT + bool unsat{false}; // If true then the stack of frames with this frame at top is UNSAT PushFrame(PushFrame const &) = delete; PushFrame(PushFrame &&) = default; - explicit PushFrame(uint32_t id) : id(id), unsat(false) {} + explicit PushFrame(uint32_t id) : id(id) {} + private: + FrameId id; }; class AssertionStack { - private: - std::vector frames; - uint32_t frameId = 0; - public: [[nodiscard]] PushFrame const & last() const { assert(not frames.empty()); @@ -104,11 +150,12 @@ class MainSolver { assert(frameCount() > 0); last().push(fla); } + private: + std::vector frames; + uint32_t frameId = 0; }; class Substitutions { - std::vector perFrameSubst; - public: void push() { perFrameSubst.emplace_back(); } void pop() { perFrameSubst.pop_back(); } @@ -127,15 +174,25 @@ class MainSolver { } return allSubst; } + private: + std::vector perFrameSubst; }; -/** Actual MainSolver members **/ -protected: - AssertionStack frames; - Substitutions substitutions; - vec frameTerms; - std::size_t firstNotSimplifiedFrame = 0; - unsigned int insertedFormulasCount = 0; - sstat status = s_Undef; // The status of the last solver call + + struct SubstitutionResult { + Logic::SubstMap usedSubstitution; + PTRef result {PTRef_Undef}; + }; + + Theory & getTheory() { return *theory; } + Theory const & getTheory() const { return *theory; } + TermMapper & getTermMapper() const { return *term_mapper;} + PartitionManager & getPartitionManager() { return pmanager; } + + [[nodiscard]] PTRef currentRootInstance() const; + + void printFramesAsQuery(std::ostream & s) const; + + static std::unique_ptr createInnerSolver(SMTConfig& config, THandler& thandler); PTRef newFrameTerm(FrameId frameId) { assert(frameId != 0); @@ -163,88 +220,35 @@ class MainSolver { sstat giveToSolver(PTRef root, FrameId push_id); - struct SubstitutionResult { - Logic::SubstMap usedSubstitution; - PTRef result {PTRef_Undef}; - }; - PTRef applyLearntSubstitutions(PTRef fla); PTRef substitutionPass(PTRef fla, PreprocessingContext const& context); SubstitutionResult computeSubstitutions(PTRef fla); -public: + AssertionStack frames; + + sstat status = s_Undef; // The status of the last solver call + +private: + std::unique_ptr theory; std::unique_ptr term_mapper; std::unique_ptr thandler; std::unique_ptr smt_solver; - Logic& logic; + Logic & logic; PartitionManager pmanager; - SMTConfig& config; + SMTConfig & config; Tseitin ts; opensmt::OSMTTimeVal query_timer; // How much time we spend solving. std::string solver_name; // Name for the solver int check_called = 0; // A counter on how many times check was called. - sstat solve(); - - [[nodiscard]] PTRef currentRootInstance() const; - - void printFramesAsQuery(std::ostream & s) const; - - static std::unique_ptr createInnerSolver(SMTConfig& config, THandler& thandler); - - MainSolver(Logic& logic, SMTConfig& conf, std::string name); - - MainSolver(std::unique_ptr th, std::unique_ptr tm, std::unique_ptr thd, - std::unique_ptr ss, Logic & logic, SMTConfig & conf, std::string name); - - virtual ~MainSolver() = default; - MainSolver (const MainSolver&) = delete; - MainSolver& operator = (const MainSolver&) = delete; - MainSolver (MainSolver&&) = default; - MainSolver& operator = (MainSolver&&) = delete; - - SMTConfig& getConfig() { return config; } - SimpSMTSolver & getSMTSolver() { return *smt_solver; } - SimpSMTSolver const & getSMTSolver() const { return *smt_solver; } - - THandler &getTHandler() { return *thandler; } - Logic &getLogic() { return logic; } - Theory &getTheory() { return *theory; } - const Theory &getTheory() const { return *theory; } - PartitionManager & getPartitionManager(); - - void push(); - bool pop(); - void insertFormula(PTRef fla); - - void initialize(); - - virtual sstat check(); // A wrapper for solve which simplifies the loaded formulas and initializes the solvers - // Simplify frames (not yet simplified) until all are simplified or the instance is detected unsatisfiable. - sstat simplifyFormulas(); - - void printFramesAsQuery() const; - [[nodiscard]] sstat getStatus() const; - - // Values - lbool getTermValue (PTRef tr) const; - - // Returns model of the last query (must be in satisfiable state) - std::unique_ptr getModel(); - - // Prints proof of the last query (must be in unsatisfiable state) - void printResolutionProofSMT2() const; - - void stop() { smt_solver->stop = true; } - - // Returns interpolation context for the last query (must be in UNSAT state) - std::unique_ptr getInterpolationContext(); - - static std::unique_ptr createTheory(Logic & logic, SMTConfig & config); + Substitutions substitutions; + vec frameTerms; + std::size_t firstNotSimplifiedFrame = 0; + unsigned int insertedFormulasCount = 0; }; bool MainSolver::trackPartitions() const diff --git a/src/parallel/MainSplitter.cc b/src/parallel/MainSplitter.cc index 500f6b61d..26ace08c1 100644 --- a/src/parallel/MainSplitter.cc +++ b/src/parallel/MainSplitter.cc @@ -17,7 +17,7 @@ void MainSplitter::notifyResult(sstat const & result) } sstat MainSplitter::check() { - if (getChannel().isSolverInParallelMode() and not config.sat_solver_limit()) { + if (getChannel().isSolverInParallelMode() and not getConfig().sat_solver_limit()) { //push frames size should match with length of the solver branch if (frames.frameCount() != static_cast(getSplitter().getSolverBranch().size() + 1)) @@ -31,7 +31,7 @@ sstat MainSplitter::check() { } sstat MainSplitter::solve_(vec const & enabledFrames) { - if (getChannel().isSolverInParallelMode() and not config.sat_solver_limit()) { + if (getChannel().isSolverInParallelMode() and not getConfig().sat_solver_limit()) { vec> const & solverBranch = getSplitter().getSolverBranch(); if (enabledFrames.size() > solverBranch.size() + 1) { throw PTPLib::common::Exception(__FILE__, __LINE__, @@ -58,7 +58,7 @@ sstat MainSplitter::solve() { }; void MainSplitter::writeSplits(std::string const & baseName) const { - assert(config.sat_split_type() != spt_none); + assert(getConfig().sat_split_type() != spt_none); auto const & splits = getSplitter().getSplits(); auto splitStrings = getPartitionClauses(); @@ -94,6 +94,7 @@ std::unique_ptr MainSplitter::createInnerSolver(SMTConfig & confi bool MainSplitter::verifyPartitions(vec const & partitions) const { bool ok = true; std::string error; + auto & logic = getLogic(); VerificationUtils verifier(logic); for (int i = 0; i < partitions.size(); i++) { for (int j = i + 1; j < partitions.size(); j++) { @@ -108,7 +109,7 @@ bool MainSplitter::verifyPartitions(vec const & partitions) const { for (PTRef tr : partitions) { partitionCoverageQuery.push(logic.mkNot(tr)); } - if (partitions.size() == config.sat_split_num()) { + if (partitions.size() == getConfig().sat_split_num()) { // The partitions need to cover the full search space, i.e., the conjunction of the negated partitions must be unsatisfiable if (not verifier.impliesInternal(logic.mkAnd(partitionCoverageQuery), logic.getTerm_false())) { error += "[Non-covering partitioning: " + logic.pp(logic.mkAnd(partitionCoverageQuery)) + " is satisfiable] "; @@ -137,10 +138,11 @@ bool MainSplitter::verifyPartitions(vec const & partitions) const { std::vector MainSplitter::getPartitionClauses() const { assert(not isSplitTypeNone()); auto const & splits = getSplitter().getSplits(); + auto & logic = getLogic(); vec partitionsTr; partitionsTr.capacity(splits.size()); for (auto const &split : splits) { - auto conj_vec = addToConjunction(split.splitToPtAsgns(*thandler)); + auto conj_vec = addToConjunction(split.splitToPtAsgns(getTHandler())); partitionsTr.push(logic.mkAnd(conj_vec)); } @@ -157,6 +159,7 @@ std::vector MainSplitter::getPartitionClauses() const { vec MainSplitter::addToConjunction(std::vector> const & in) const { vec out; + auto & logic = getLogic(); for (const auto & constr : in) { vec disj_vec; for (const auto & pta : constr) { @@ -165,4 +168,4 @@ vec MainSplitter::addToConjunction(std::vector> const & in) c out.push(logic.mkOr(std::move(disj_vec))); } return out; -} \ No newline at end of file +} diff --git a/src/parallel/MainSplitter.h b/src/parallel/MainSplitter.h index e32a6394b..4d1bd4466 100644 --- a/src/parallel/MainSplitter.h +++ b/src/parallel/MainSplitter.h @@ -20,15 +20,17 @@ class MainSplitter : public MainSolver { private: - inline bool isSplitTypeScatter() const & { return dynamic_cast(*smt_solver).isSplitTypeScatter(); } + inline bool isSplitTypeScatter() const { return dynamic_cast(getSMTSolver()).isSplitTypeScatter(); } - inline bool isSplitTypeNone() const & { return dynamic_cast(*smt_solver).isSplitTypeNone(); } + inline bool isSplitTypeNone() const { return dynamic_cast(getSMTSolver()).isSplitTypeNone(); } inline PTPLib::net::Channel & getChannel() const { return getSplitter().getChannel(); } - inline ScatterSplitter & getScatterSplitter() { return dynamic_cast(getSMTSolver()); } + inline ScatterSplitter const & getScatterSplitter() const { return dynamic_cast(getSMTSolver()); } + inline ScatterSplitter & getScatterSplitter() { return dynamic_cast(getSMTSolver()); } - inline Splitter & getSplitter() const { return dynamic_cast(*smt_solver); } + inline Splitter const & getSplitter() const { return dynamic_cast(getSMTSolver()); } + inline Splitter & getSplitter() { return dynamic_cast(getSMTSolver()); } void notifyResult(sstat const & result); @@ -58,8 +60,6 @@ class MainSplitter : public MainSolver { void writeSplits(std::string const &) const; static std::unique_ptr createInnerSolver(SMTConfig &, THandler &, PTPLib::net::Channel &); - - inline TermMapper& getTermMapper() const { return *term_mapper;} }; diff --git a/src/parallel/Splitter.h b/src/parallel/Splitter.h index 2b8626ff8..daa56f76b 100644 --- a/src/parallel/Splitter.h +++ b/src/parallel/Splitter.h @@ -32,7 +32,7 @@ class Splitter { , channel(ch) {} - std::vector const & getSplits() { return splitContext.getSplits(); } + std::vector const & getSplits() const { return splitContext.getSplits(); } bool isSplitTypeScatter() const { return splitContext.isSplitTypeScatter(); } diff --git a/test/unit/test_UFInterpolation.cc b/test/unit/test_UFInterpolation.cc index 0e7be4c02..1b7491a05 100644 --- a/test/unit/test_UFInterpolation.cc +++ b/test/unit/test_UFInterpolation.cc @@ -7,10 +7,6 @@ #include #include "VerificationUtils.h" -bool verifyInterpolant(PTRef itp, PartitionManager & pManager, ipartitions_t const & Amask, Logic & logic) { - return VerificationUtils(logic).verifyInterpolantInternal(pManager.getPartition(Amask, PartitionManager::part::A), pManager.getPartition(Amask, PartitionManager::part::B), itp); -} - class UFInterpolationTest : public ::testing::Test { protected: UFInterpolationTest(): logic{opensmt::Logic_t::QF_UF} {} @@ -42,8 +38,14 @@ class UFInterpolationTest : public ::testing::Test { PTRef x, y, x1, x2, x3, x4, y1, y2, z1, z2, z3, z4, z5, z6, z7, z8; SymRef f, g, p; - bool verifyInterpolant(PTRef itp, PartitionManager & pManager, ipartitions_t const & Amask) { - return ::verifyInterpolant(itp, pManager, Amask, logic); + MainSolver makeSolver() { + const char* msg = "ok"; + config.setOption(SMTConfig::o_produce_inter, SMTOption(true), msg); + return {logic, config, "ufinterpolator"}; + } + + bool verifyInterpolant(PTRef A, PTRef B, PTRef itp) { + return VerificationUtils(logic).verifyInterpolantInternal(A, B, itp); } }; @@ -54,12 +56,11 @@ TEST_F(UFInterpolationTest, test_SimpleTransitivity){ PTRef eq1 = logic.mkEq(x,y); PTRef eq2 = logic.mkEq(y,z1); PTRef eq3 = logic.mkEq(z1,x); - const char* msg = "ok"; - config.setOption(SMTConfig::o_produce_inter, SMTOption(true), msg); - MainSolver solver(logic, config, "ufinterpolator"); + PTRef neq3 = logic.mkNot(eq3); + auto solver = makeSolver(); solver.insertFormula(eq1); solver.insertFormula(eq2); - solver.insertFormula(logic.mkNot(eq3)); + solver.insertFormula(neq3); auto res = solver.check(); ASSERT_EQ(res, s_False); auto itpCtx = solver.getInterpolationContext(); @@ -67,11 +68,11 @@ TEST_F(UFInterpolationTest, test_SimpleTransitivity){ ipartitions_t mask; opensmt::setbit(mask, 0); itpCtx->getSingleInterpolant(interpolants, mask); - EXPECT_TRUE(verifyInterpolant(interpolants[0], solver.getPartitionManager(), mask)); + EXPECT_TRUE(verifyInterpolant(eq1, logic.mkAnd(eq2, neq3), interpolants[0])); interpolants.clear(); opensmt::setbit(mask, 1); itpCtx->getSingleInterpolant(interpolants, mask); - EXPECT_TRUE(verifyInterpolant(interpolants[0], solver.getPartitionManager(), mask)); + EXPECT_TRUE(verifyInterpolant(logic.mkAnd(eq1, eq2), neq3, interpolants[0])); } TEST_F(UFInterpolationTest, test_SimpleTransitivityReversed){ @@ -81,10 +82,9 @@ TEST_F(UFInterpolationTest, test_SimpleTransitivityReversed){ PTRef eq1 = logic.mkEq(x,y); PTRef eq2 = logic.mkEq(y,z1); PTRef eq3 = logic.mkEq(z1,x); - const char* msg = "ok"; - config.setOption(SMTConfig::o_produce_inter, SMTOption(true), msg); - MainSolver solver(logic, config, "ufinterpolator"); - solver.insertFormula(logic.mkNot(eq3)); + PTRef neq3 = logic.mkNot(eq3); + auto solver = makeSolver(); + solver.insertFormula(neq3); solver.insertFormula(eq2); solver.insertFormula(eq1); auto res = solver.check(); @@ -94,11 +94,11 @@ TEST_F(UFInterpolationTest, test_SimpleTransitivityReversed){ ipartitions_t mask; opensmt::setbit(mask, 0); itpCtx->getSingleInterpolant(interpolants, mask); - EXPECT_TRUE(verifyInterpolant(interpolants[0], solver.getPartitionManager(), mask)); + EXPECT_TRUE(verifyInterpolant(neq3, logic.mkAnd(eq2, eq1), interpolants[0])); interpolants.clear(); opensmt::setbit(mask, 1); itpCtx->getSingleInterpolant(interpolants, mask); - EXPECT_TRUE(verifyInterpolant(interpolants[0], solver.getPartitionManager(), mask)); + EXPECT_TRUE(verifyInterpolant(logic.mkAnd(neq3, eq2), eq1, interpolants[0])); } TEST_F(UFInterpolationTest, test_SimpleCongruence){ @@ -107,11 +107,12 @@ TEST_F(UFInterpolationTest, test_SimpleCongruence){ */ PTRef eq1 = logic.mkEq(x,y); PTRef eq2 = logic.mkEq(logic.mkUninterpFun(f, {x}), logic.mkUninterpFun(f, {y})); - const char* msg = "ok"; - config.setOption(SMTConfig::o_produce_inter, SMTOption(true), msg); - MainSolver solver(logic, config, "ufinterpolator"); - solver.insertFormula(eq1); - solver.insertFormula(logic.mkNot(eq2)); + PTRef neq2 = logic.mkNot(eq2); + PTRef A = eq1; + PTRef B = neq2; + auto solver = makeSolver(); + solver.insertFormula(A); + solver.insertFormula(B); auto res = solver.check(); ASSERT_EQ(res, s_False); auto itpCtx = solver.getInterpolationContext(); @@ -119,7 +120,7 @@ TEST_F(UFInterpolationTest, test_SimpleCongruence){ ipartitions_t mask; opensmt::setbit(mask, 0); itpCtx->getSingleInterpolant(interpolants, mask); - EXPECT_TRUE(verifyInterpolant(interpolants[0], solver.getPartitionManager(), mask)); + EXPECT_TRUE(verifyInterpolant(A, B, interpolants[0])); } TEST_F(UFInterpolationTest, test_SimpleCongruenceReversed){ @@ -128,11 +129,12 @@ TEST_F(UFInterpolationTest, test_SimpleCongruenceReversed){ */ PTRef eq1 = logic.mkEq(x,y); PTRef eq2 = logic.mkEq(logic.mkUninterpFun(f, {x}), logic.mkUninterpFun(f, {y})); - const char* msg = "ok"; - config.setOption(SMTConfig::o_produce_inter, SMTOption(true), msg); - MainSolver solver(logic, config, "ufinterpolator"); - solver.insertFormula(logic.mkNot(eq2)); - solver.insertFormula(eq1); + PTRef neq2 = logic.mkNot(eq2); + PTRef A = neq2; + PTRef B = eq1; + auto solver = makeSolver(); + solver.insertFormula(A); + solver.insertFormula(B); auto res = solver.check(); ASSERT_EQ(res, s_False); auto itpCtx = solver.getInterpolationContext(); @@ -140,7 +142,7 @@ TEST_F(UFInterpolationTest, test_SimpleCongruenceReversed){ ipartitions_t mask; opensmt::setbit(mask, 0); itpCtx->getSingleInterpolant(interpolants, mask); - EXPECT_TRUE(verifyInterpolant(interpolants[0], solver.getPartitionManager(), mask)); + EXPECT_TRUE(verifyInterpolant(A, B, interpolants[0])); } TEST_F(UFInterpolationTest, test_NotImmediatelyColorableCGraph){ @@ -151,11 +153,11 @@ TEST_F(UFInterpolationTest, test_NotImmediatelyColorableCGraph){ PTRef eqA2 = logic.mkEq(logic.mkUninterpFun(g, {x,z2}),z3); PTRef eqB1 = logic.mkEq(y,z2); PTRef eqB2 = logic.mkEq(logic.mkUninterpFun(g, {z1,y}),z3); - const char* msg = "ok"; - config.setOption(SMTConfig::o_produce_inter, SMTOption(true), msg); - MainSolver solver(logic, config, "ufinterpolator"); - solver.insertFormula(logic.mkAnd(eqA1, eqA2)); - solver.insertFormula(logic.mkAnd(eqB1, logic.mkNot(eqB2))); + PTRef A = logic.mkAnd(eqA1, eqA2); + PTRef B = logic.mkAnd(eqB1, logic.mkNot(eqB2)); + auto solver = makeSolver(); + solver.insertFormula(A); + solver.insertFormula(B); auto res = solver.check(); ASSERT_EQ(res, s_False); auto itpCtx = solver.getInterpolationContext(); @@ -163,12 +165,12 @@ TEST_F(UFInterpolationTest, test_NotImmediatelyColorableCGraph){ ipartitions_t mask; opensmt::setbit(mask, 0); itpCtx->getSingleInterpolant(interpolants, mask); - EXPECT_TRUE(verifyInterpolant(interpolants[0], solver.getPartitionManager(), mask)); + EXPECT_TRUE(verifyInterpolant(A, B, interpolants[0])); // change the interpolation algorithm config.setEUFInterpolationAlgorithm(itp_euf_alg_weak); interpolants.clear(); itpCtx->getSingleInterpolant(interpolants, mask); - EXPECT_TRUE(verifyInterpolant(interpolants[0], solver.getPartitionManager(), mask)); + EXPECT_TRUE(verifyInterpolant(A, B, interpolants[0])); } TEST_F(UFInterpolationTest, test_NotImmediatelyColorableCGraphReversed){ @@ -180,11 +182,11 @@ TEST_F(UFInterpolationTest, test_NotImmediatelyColorableCGraphReversed){ PTRef eqB2 = logic.mkEq(logic.mkUninterpFun(g, {x,z2}),z3); PTRef eqA1 = logic.mkEq(y,z2); PTRef eqA2 = logic.mkEq(logic.mkUninterpFun(g, {z1,y}),z3); - const char* msg = "ok"; - config.setOption(SMTConfig::o_produce_inter, SMTOption(true), msg); - MainSolver solver(logic, config, "ufinterpolator"); - solver.insertFormula(logic.mkAnd(eqA1, logic.mkNot(eqA2))); - solver.insertFormula(logic.mkAnd(eqB1, eqB2)); + PTRef A = logic.mkAnd(eqA1, logic.mkNot(eqA2)); + PTRef B = logic.mkAnd(eqB1, eqB2); + auto solver = makeSolver(); + solver.insertFormula(A); + solver.insertFormula(B); auto res = solver.check(); ASSERT_EQ(res, s_False); auto itpCtx = solver.getInterpolationContext(); @@ -192,12 +194,12 @@ TEST_F(UFInterpolationTest, test_NotImmediatelyColorableCGraphReversed){ ipartitions_t mask; opensmt::setbit(mask, 0); itpCtx->getSingleInterpolant(interpolants, mask); - EXPECT_TRUE(verifyInterpolant(interpolants[0], solver.getPartitionManager(), mask)); + EXPECT_TRUE(verifyInterpolant(A, B, interpolants[0])); // change the interpolation algorithm config.setEUFInterpolationAlgorithm(itp_euf_alg_weak); interpolants.clear(); itpCtx->getSingleInterpolant(interpolants, mask); - EXPECT_TRUE(verifyInterpolant(interpolants[0], solver.getPartitionManager(), mask)); + EXPECT_TRUE(verifyInterpolant(A, B, interpolants[0])); } TEST_F(UFInterpolationTest, test_JustificationRequired){ @@ -219,11 +221,11 @@ TEST_F(UFInterpolationTest, test_JustificationRequired){ PTRef eqB4 = logic.mkEq(y1,z7); PTRef eqB5 = logic.mkEq(z8,y2); PTRef eqB6 = logic.mkEq(y1,y2); - const char* msg = "ok"; - config.setOption(SMTConfig::o_produce_inter, SMTOption(true), msg); - MainSolver solver(logic, config, "ufinterpolator"); - solver.insertFormula(logic.mkAnd({eqA1, eqA2, eqA3, eqA4, eqA5, eqA6, eqA7, eqA8})); - solver.insertFormula(logic.mkAnd({eqB1, eqB2, eqB3, eqB4, eqB5, logic.mkNot(eqB6)})); + PTRef A = logic.mkAnd({eqA1, eqA2, eqA3, eqA4, eqA5, eqA6, eqA7, eqA8}); + PTRef B = logic.mkAnd({eqB1, eqB2, eqB3, eqB4, eqB5, logic.mkNot(eqB6)}); + auto solver = makeSolver(); + solver.insertFormula(A); + solver.insertFormula(B); auto res = solver.check(); ASSERT_EQ(res, s_False); auto itpCtx = solver.getInterpolationContext(); @@ -231,12 +233,12 @@ TEST_F(UFInterpolationTest, test_JustificationRequired){ ipartitions_t mask; opensmt::setbit(mask, 0); itpCtx->getSingleInterpolant(interpolants, mask); - EXPECT_TRUE(verifyInterpolant(interpolants[0], solver.getPartitionManager(), mask)); + EXPECT_TRUE(verifyInterpolant(A, B, interpolants[0])); // change the interpolation algorithm config.setEUFInterpolationAlgorithm(itp_euf_alg_weak); interpolants.clear(); itpCtx->getSingleInterpolant(interpolants, mask); - EXPECT_TRUE(verifyInterpolant(interpolants[0], solver.getPartitionManager(), mask)); + EXPECT_TRUE(verifyInterpolant(A, B, interpolants[0])); } TEST_F(UFInterpolationTest, test_JustificationRequiredReversed){ @@ -259,11 +261,11 @@ TEST_F(UFInterpolationTest, test_JustificationRequiredReversed){ PTRef eqA4 = logic.mkEq(y1,z7); PTRef eqA5 = logic.mkEq(z8,y2); PTRef eqA6 = logic.mkEq(y1,y2); - const char* msg = "ok"; - config.setOption(SMTConfig::o_produce_inter, SMTOption(true), msg); - MainSolver solver(logic, config, "ufinterpolator"); - solver.insertFormula(logic.mkAnd({eqA1, eqA2, eqA3, eqA4, eqA5, logic.mkNot(eqA6)})); - solver.insertFormula(logic.mkAnd({eqB1, eqB2, eqB3, eqB4, eqB5, eqB6, eqB7,eqB8})); + PTRef A = logic.mkAnd({eqA1, eqA2, eqA3, eqA4, eqA5, logic.mkNot(eqA6)}); + PTRef B = logic.mkAnd({eqB1, eqB2, eqB3, eqB4, eqB5, eqB6, eqB7,eqB8}); + auto solver = makeSolver(); + solver.insertFormula(A); + solver.insertFormula(B); auto res = solver.check(); ASSERT_EQ(res, s_False); auto itpCtx = solver.getInterpolationContext(); @@ -271,12 +273,12 @@ TEST_F(UFInterpolationTest, test_JustificationRequiredReversed){ ipartitions_t mask; opensmt::setbit(mask, 0); itpCtx->getSingleInterpolant(interpolants, mask); - EXPECT_TRUE(verifyInterpolant(interpolants[0], solver.getPartitionManager(), mask)); + EXPECT_TRUE(verifyInterpolant(A, B, interpolants[0])); // change the interpolation algorithm config.setEUFInterpolationAlgorithm(itp_euf_alg_weak); interpolants.clear(); itpCtx->getSingleInterpolant(interpolants, mask); - EXPECT_TRUE(verifyInterpolant(interpolants[0], solver.getPartitionManager(), mask)); + EXPECT_TRUE(verifyInterpolant(A, B, interpolants[0])); } TEST_F(UFInterpolationTest, test_SimpleUninterpretedPredicate){ @@ -286,12 +288,11 @@ TEST_F(UFInterpolationTest, test_SimpleUninterpretedPredicate){ PTRef eq = logic.mkEq(x,y); PTRef px = logic.mkUninterpFun(p, {x}); PTRef py = logic.mkUninterpFun(p, {y}); - const char* msg = "ok"; - config.setOption(SMTConfig::o_produce_inter, SMTOption(true), msg); - MainSolver solver(logic, config, "ufinterpolator"); + PTRef npy = logic.mkNot(py); + auto solver = makeSolver(); solver.insertFormula(px); solver.insertFormula(eq); - solver.insertFormula(logic.mkNot(py)); + solver.insertFormula(npy); auto res = solver.check(); ASSERT_EQ(res, s_False); auto itpCtx = solver.getInterpolationContext(); @@ -299,7 +300,7 @@ TEST_F(UFInterpolationTest, test_SimpleUninterpretedPredicate){ ipartitions_t mask; opensmt::setbit(mask, 0); itpCtx->getSingleInterpolant(interpolants, mask); - EXPECT_TRUE(verifyInterpolant(interpolants[0], solver.getPartitionManager(), mask)); + EXPECT_TRUE(verifyInterpolant(px, logic.mkAnd(eq, npy), interpolants[0])); } TEST_F(UFInterpolationTest, test_ConstantsConflict){ @@ -310,11 +311,11 @@ TEST_F(UFInterpolationTest, test_ConstantsConflict){ PTRef d = logic.mkConst(ufsort, "d"); PTRef eqA = logic.mkEq(c,x); PTRef eqB = logic.mkEq(x,d); - const char* msg = "ok"; - config.setOption(SMTConfig::o_produce_inter, SMTOption(true), msg); - MainSolver solver(logic, config, "ufinterpolator"); - solver.insertFormula(eqA); - solver.insertFormula(eqB); + PTRef A = eqA; + PTRef B = eqB; + auto solver = makeSolver(); + solver.insertFormula(A); + solver.insertFormula(B); auto res = solver.check(); ASSERT_EQ(res, s_False); auto itpCtx = solver.getInterpolationContext(); @@ -322,7 +323,7 @@ TEST_F(UFInterpolationTest, test_ConstantsConflict){ ipartitions_t mask; opensmt::setbit(mask, 0); itpCtx->getSingleInterpolant(interpolants, mask); - EXPECT_TRUE(verifyInterpolant(interpolants[0], solver.getPartitionManager(), mask)); + EXPECT_TRUE(verifyInterpolant(A, B, interpolants[0])); } TEST_F(UFInterpolationTest, test_TwoLevelJustification){ @@ -337,11 +338,11 @@ TEST_F(UFInterpolationTest, test_TwoLevelJustification){ PTRef eqA2 = logic.mkEq(logic.mkUninterpFun(f, {z2}), x2); PTRef eqA3 = logic.mkEq(z3,z4); PTRef dis = logic.mkNot(logic.mkEq(x1, x2)); - const char* msg = "ok"; - config.setOption(SMTConfig::o_produce_inter, SMTOption(true), msg); - MainSolver solver(logic, config, "ufinterpolator"); - solver.insertFormula(logic.mkAnd({eqA1, eqA2, eqA3, dis})); - solver.insertFormula(logic.mkAnd({eqB1, eqB2})); + PTRef A = logic.mkAnd({eqA1, eqA2, eqA3, dis}); + PTRef B = logic.mkAnd({eqB1, eqB2}); + auto solver = makeSolver(); + solver.insertFormula(A); + solver.insertFormula(B); auto res = solver.check(); ASSERT_EQ(res, s_False); auto itpCtx = solver.getInterpolationContext(); @@ -349,12 +350,12 @@ TEST_F(UFInterpolationTest, test_TwoLevelJustification){ ipartitions_t mask; opensmt::setbit(mask, 0); itpCtx->getSingleInterpolant(interpolants, mask); - EXPECT_TRUE(verifyInterpolant(interpolants[0], solver.getPartitionManager(), mask)); + EXPECT_TRUE(verifyInterpolant(A, B, interpolants[0])); // change the interpolation algorithm config.setEUFInterpolationAlgorithm(itp_euf_alg_weak); interpolants.clear(); itpCtx->getSingleInterpolant(interpolants, mask); - EXPECT_TRUE(verifyInterpolant(interpolants[0], solver.getPartitionManager(), mask)); + EXPECT_TRUE(verifyInterpolant(A, B, interpolants[0])); } TEST_F(UFInterpolationTest, test_TwoLevelJustificationDiseqInB){ @@ -369,11 +370,11 @@ TEST_F(UFInterpolationTest, test_TwoLevelJustificationDiseqInB){ PTRef eqA2 = logic.mkEq(logic.mkUninterpFun(f, {z2}), x2); PTRef eqA3 = logic.mkEq(z3,z4); PTRef dis = logic.mkNot(logic.mkEq(x1, x2)); - const char* msg = "ok"; - config.setOption(SMTConfig::o_produce_inter, SMTOption(true), msg); - MainSolver solver(logic, config, "ufinterpolator"); - solver.insertFormula(logic.mkAnd({eqA1, eqA2, eqA3})); - solver.insertFormula(logic.mkAnd({eqB1, eqB2, dis})); + PTRef A = logic.mkAnd({eqA1, eqA2, eqA3}); + PTRef B = logic.mkAnd({eqB1, eqB2, dis}); + auto solver = makeSolver(); + solver.insertFormula(A); + solver.insertFormula(B); auto res = solver.check(); ASSERT_EQ(res, s_False); auto itpCtx = solver.getInterpolationContext(); @@ -381,12 +382,12 @@ TEST_F(UFInterpolationTest, test_TwoLevelJustificationDiseqInB){ ipartitions_t mask; opensmt::setbit(mask, 0); itpCtx->getSingleInterpolant(interpolants, mask); - EXPECT_TRUE(verifyInterpolant(interpolants[0], solver.getPartitionManager(), mask)); + EXPECT_TRUE(verifyInterpolant(A, B, interpolants[0])); // change the interpolation algorithm config.setEUFInterpolationAlgorithm(itp_euf_alg_weak); interpolants.clear(); itpCtx->getSingleInterpolant(interpolants, mask); - EXPECT_TRUE(verifyInterpolant(interpolants[0], solver.getPartitionManager(), mask)); + EXPECT_TRUE(verifyInterpolant(A, B, interpolants[0])); } TEST_F(UFInterpolationTest, test_LocalColorInformationInsufficient){ @@ -397,7 +398,6 @@ TEST_F(UFInterpolationTest, test_LocalColorInformationInsufficient){ */ // Note: this requires a set-up in specific order, different from the set-up we have in UFInterpolationTest - Logic logic{opensmt::Logic_t::QF_UF}; SRef ufsort = logic.declareUninterpretedSort("U"); SymRef P = logic.declareFun("P", logic.getSort_bool(), {ufsort}); SymRef f = logic.declareFun("f", ufsort, {ufsort, ufsort}); @@ -422,7 +422,8 @@ TEST_F(UFInterpolationTest, test_LocalColorInformationInsufficient){ PTRef f_x_y = logic.mkUninterpFun(f, {x,y}); PTRef P_f = logic.mkUninterpFun(P, {f_x_y}); PTRef eqB1 = logic.mkEq(r1, f_a1_b1); - PTRef eqB2 = logic.mkEq(r2,f_a2_b2); + PTRef eqB2 = logic.mkEq(r2, f_a2_b2); + PTRef B = logic.mkAnd(eqB1, eqB2); PTRef A = logic.mkAnd({ P_f, logic.mkEq(a1, x), @@ -432,10 +433,8 @@ TEST_F(UFInterpolationTest, test_LocalColorInformationInsufficient){ logic.mkNot(logic.mkEq(r1, r2)) }); - const char* msg = "ok"; - config.setOption(SMTConfig::o_produce_inter, SMTOption(true), msg); - MainSolver solver(logic, config, "ufinterpolator"); - solver.insertFormula(logic.mkAnd(eqB1, eqB2)); + auto solver = makeSolver(); + solver.insertFormula(B); solver.insertFormula(A); auto res = solver.check(); ASSERT_EQ(res, s_False); @@ -445,7 +444,7 @@ TEST_F(UFInterpolationTest, test_LocalColorInformationInsufficient){ opensmt::setbit(mask, 1); itpCtx->getSingleInterpolant(interpolants, mask); // std::cout << logic.printTerm(interpolants[0]) << std::endl; - EXPECT_TRUE(::verifyInterpolant(interpolants[0], solver.getPartitionManager(), mask, logic)); + EXPECT_TRUE(verifyInterpolant(A, B, interpolants[0])); } TEST_F(UFInterpolationTest, test_DistinctInA){ @@ -456,11 +455,11 @@ TEST_F(UFInterpolationTest, test_DistinctInA){ PTRef eqA1 = logic.mkEq(x1,x2); PTRef eqA2 = logic.mkEq(x2,x3); PTRef deqB = logic.mkDistinct({x1,x4,x3}); - const char* msg = "ok"; - config.setOption(SMTConfig::o_produce_inter, SMTOption(true), msg); - MainSolver solver(logic, config, "ufinterpolator"); - solver.insertFormula(logic.mkAnd(eqA1, eqA2)); - solver.insertFormula(deqB); + PTRef A = logic.mkAnd(eqA1, eqA2); + PTRef B = deqB; + auto solver = makeSolver(); + solver.insertFormula(A); + solver.insertFormula(B); auto res = solver.check(); ASSERT_EQ(res, s_False); auto itpCtx = solver.getInterpolationContext(); @@ -469,8 +468,8 @@ TEST_F(UFInterpolationTest, test_DistinctInA){ itpCtx->getSingleInterpolant(interpolants, mask); PTRef itp = interpolants[0]; // std::cout << "Interpolant: " << logic.pp(itp) << std::endl; - EXPECT_TRUE(verifyInterpolant(itp, solver.getPartitionManager(), mask)); - ASSERT_EQ(itp, logic.mkEq(x1,x3)); + EXPECT_TRUE(verifyInterpolant(A, B, itp)); + ASSERT_EQ(itp, logic.mkEq(x1, x3)); } TEST_F(UFInterpolationTest, test_DistinctInB){ @@ -481,11 +480,11 @@ TEST_F(UFInterpolationTest, test_DistinctInB){ PTRef eqB1 = logic.mkEq(x1,x2); PTRef eqB2 = logic.mkEq(x2,x3); PTRef deqA = logic.mkDistinct({x1,x4,x3}); - const char* msg = "ok"; - config.setOption(SMTConfig::o_produce_inter, SMTOption(true), msg); - MainSolver solver(logic, config, "ufinterpolator"); - solver.insertFormula(deqA); - solver.insertFormula(logic.mkAnd(eqB1, eqB2)); + PTRef A = deqA; + PTRef B = logic.mkAnd(eqB1, eqB2); + auto solver = makeSolver(); + solver.insertFormula(A); + solver.insertFormula(B); auto res = solver.check(); ASSERT_EQ(res, s_False); auto itpCtx = solver.getInterpolationContext(); @@ -494,8 +493,6 @@ TEST_F(UFInterpolationTest, test_DistinctInB){ itpCtx->getSingleInterpolant(interpolants, mask); PTRef itp = interpolants[0]; // std::cout << "Interpolant: " << logic.pp(itp) << std::endl; - EXPECT_TRUE(verifyInterpolant(itp, solver.getPartitionManager(), mask)); - ASSERT_EQ(itp, logic.mkNot(logic.mkEq(x1,x3))); + EXPECT_TRUE(verifyInterpolant(A, B, itp)); + ASSERT_EQ(itp, logic.mkNot(logic.mkEq(x1, x3))); } - -