Adds support for incrementality + get-interpol, including the get-interpol-next command.
{
CVC5_API_TRY_CATCH_BEGIN;
CVC5_API_SOLVER_CHECK_TERM(conj);
+ CVC5_API_CHECK(d_slv->getOptions().smt.produceInterpols
+ != options::ProduceInterpols::NONE)
+ << "Cannot get interpolant unless interpolants are enabled (try "
+ "--produce-interpols=mode)";
//////// all checks before this line
Node result;
- bool success = d_slv->getInterpol(*conj.d_node, result);
+ TypeNode nullType;
+ bool success = d_slv->getInterpolant(*conj.d_node, nullType, result);
if (success)
{
output = Term(this, result);
{
CVC5_API_TRY_CATCH_BEGIN;
CVC5_API_SOLVER_CHECK_TERM(conj);
+ CVC5_API_CHECK(d_slv->getOptions().smt.produceInterpols
+ != options::ProduceInterpols::NONE)
+ << "Cannot get interpolant unless interpolants are enabled (try "
+ "--produce-interpols=mode)";
//////// all checks before this line
Node result;
bool success =
- d_slv->getInterpol(*conj.d_node, *grammar.resolve().d_type, result);
+ d_slv->getInterpolant(*conj.d_node, *grammar.resolve().d_type, result);
+ if (success)
+ {
+ output = Term(this, result);
+ }
+ return success;
+ ////////
+ CVC5_API_TRY_CATCH_END;
+}
+
+bool Solver::getInterpolantNext(Term& output) const
+{
+ CVC5_API_TRY_CATCH_BEGIN;
+ CVC5_API_CHECK(d_slv->getOptions().smt.produceInterpols
+ != options::ProduceInterpols::NONE)
+ << "Cannot get interpolant unless interpolants are enabled (try "
+ "--produce-interpols=mode)";
+ CVC5_API_CHECK(d_slv->getOptions().base.incrementalSolving)
+ << "Cannot get next interpolant when not solving incrementally (try "
+ "--incremental)";
+ //////// all checks before this line
+ Node result;
+ bool success = d_slv->getInterpolantNext(result);
if (success)
{
output = Term(this, result);
*
* (get-interpol <conj>)
*
- * Requires to enable option
- * :ref:`produce-interpols <lbl-option-produce-interpols>`.
+ * Requires option
+ * :ref:`produce-interpols <lbl-option-produce-interpols>` to be set to a
+ * mode different from `none`.
* \endverbatim
*
* @param conj the conjecture term
*
* (get-interpol <conj> <grammar>)
*
- * Requires to enable option
- * :ref:`produce-interpols <lbl-option-produce-interpols>`.
+ * Requires option
+ * :ref:`produce-interpols <lbl-option-produce-interpols>` to be set to a
+ * mode different from `none`.
* \endverbatim
*
* @param conj the conjecture term
*/
bool getInterpolant(const Term& conj, Grammar& grammar, Term& output) const;
+ /**
+ * Get the next interpolant. Can only be called immediately after a successful
+ * call to get-interpol or get-interpol-next. Is guaranteed to produce a
+ * syntactically different interpolant wrt the last returned interpolant if
+ * successful.
+ *
+ * SMT-LIB:
+ *
+ * \verbatim embed:rst:leading-asterisk
+ * .. code:: smtlib
+ *
+ * (get-interpol-next)
+ *
+ * Requires to enable incremental mode, and option
+ * :ref:`produce-interpols <lbl-option-produce-interpols>` to be set to a
+ * mode different from `none`.
+ * \endverbatim
+ *
+ * @param output a Term I such that A->I and I->B are valid, where A is the
+ * current set of assertions and B is given in the input by conj
+ * on the last call to getInterpolant.
+ * @return true if it gets interpolant @f$C@f$ successfully, false otherwise
+ */
+ bool getInterpolantNext(Term& output) const;
+
/**
* Get an abduct.
*
* {@code
* ( get-interpol <conj> )
* }
- * Requires to enable option 'produce-interpols'.
+ * Requires 'produce-interpols' to be set to a mode different from 'none'.
* @param conj the conjecture term
* @param output a Term I such that {@code A->I} and {@code I->B} are valid, where A is the
* current set of assertions and B is given in the input by conj.
* {@code
* ( get-interpol <conj> <g> )
* }
- * Requires to enable option 'produce-interpols'.
+ * Requires 'produce-interpols' to be set to a mode different from 'none'.
* @param conj the conjecture term
* @param grammar the grammar for the interpolant I
* @param output a Term I such that {@code A->I} and {@code I->B} are valid, where A is the
private native boolean getInterpolant(
long pointer, long conjPointer, long grammarPointer, long outputPointer);
+ /**
+ * Get the next interpolant. Can only be called immediately after a successful
+ * call to get-interpol or get-interpol-next. Is guaranteed to produce a
+ * syntactically different interpolant wrt the last returned interpolant if
+ * successful.
+ *
+ * SMT-LIB:
+ *
+ * \verbatim embed:rst:leading-asterisk
+ * .. code:: smtlib
+ *
+ * (get-interpol-next)
+ *
+ * Requires to enable incremental mode, and option 'produce-interpols' to be
+ * set to a mode different from 'none'.
+ * \endverbatim
+ *
+ * @param output a Term I such that {@code A->I} and {@code I->B} are valid,
+ * where A is the current set of assertions and B is given in the input
+ * by conj on the last call to getInterpolant.
+ * @return true if it gets interpolant @f$C@f$ successfully, false otherwise
+ */
+ public boolean getInterpolantNext(Term output)
+ {
+ return getInterpolantNext(pointer, output.getPointer());
+ }
+
+ private native boolean getInterpolantNext(long pointer, long outputPointer);
+
/**
* Get an abduct.
* SMT-LIB:
CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, 0);
}
+/*
+ * Class: io_github_cvc5_api_Solver
+ * Method: getInterpolantNext
+ * Signature: (JJ)Z
+ */
+JNIEXPORT jboolean JNICALL Java_io_github_cvc5_api_Solver_getInterpolantNext(
+ JNIEnv* env, jobject, jlong pointer, jlong outputPointer)
+{
+ CVC5_JAVA_API_TRY_CATCH_BEGIN;
+ Solver* solver = reinterpret_cast<Solver*>(pointer);
+ Term* output = reinterpret_cast<Term*>(outputPointer);
+ return (jboolean)solver->getInterpolantNext(*output);
+ CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, 0);
+}
+
/*
* Class: io_github_cvc5_api_Solver
* Method: getAbduct
{
cmd->reset(new GetInterpolCommand(name, e, g));
}
+ | GET_INTERPOL_NEXT_TOK {
+ PARSER_STATE->checkThatLogicIsSet();
+ cmd->reset(new GetInterpolNextCommand);
+ }
| DECLARE_HEAP LPAREN_TOK
sortSymbol[t, CHECK_DECLARED]
sortSymbol[s, CHECK_DECLARED]
GET_ABDUCT_TOK : 'get-abduct';
GET_ABDUCT_NEXT_TOK : 'get-abduct-next';
GET_INTERPOL_TOK : 'get-interpol';
+GET_INTERPOL_NEXT_TOK : 'get-interpol-next';
DECLARE_HEAP : 'declare-heap';
DECLARE_POOL : 'declare-pool';
printUnknownCommand(out, "get-interpol");
}
+void Printer::toStreamCmdGetInterpolNext(std::ostream& out) const
+{
+ printUnknownCommand(out, "get-interpol-next");
+}
+
void Printer::toStreamCmdGetAbduct(std::ostream& out,
const std::string& name,
Node conj,
Node conj,
TypeNode sygusType) const;
+ /** Print get-interpol-next command */
+ virtual void toStreamCmdGetInterpolNext(std::ostream& out) const;
+
/** Print get-abduct command */
virtual void toStreamCmdGetAbduct(std::ostream& out,
const std::string& name,
out << ')' << std::endl;
}
+void Smt2Printer::toStreamCmdGetInterpolNext(std::ostream& out) const
+{
+ out << "(get-interpol-next)" << std::endl;
+}
+
void Smt2Printer::toStreamCmdGetAbduct(std::ostream& out,
const std::string& name,
Node conj,
Node conj,
TypeNode sygusType) const override;
+ /** Print get-interpol-next command */
+ void toStreamCmdGetInterpolNext(std::ostream& out) const override;
+
/** Print get-abduct command */
void toStreamCmdGetAbduct(std::ostream& out,
const std::string& name,
{
try
{
+ // we must remember the name of the interpolant, in case get-interpol-next
+ // is called later.
+ sm->setLastSynthName(d_name);
if (d_sygus_grammar == nullptr)
{
d_resultStatus = solver->getInterpolant(d_conj, d_result);
out, d_name, termToNode(d_conj), grammarToTypeNode(d_sygus_grammar));
}
+/* -------------------------------------------------------------------------- */
+/* class GetInterpolNextCommand */
+/* -------------------------------------------------------------------------- */
+
+GetInterpolNextCommand::GetInterpolNextCommand() : d_resultStatus(false) {}
+
+api::Term GetInterpolNextCommand::getResult() const { return d_result; }
+
+void GetInterpolNextCommand::invoke(api::Solver* solver, SymbolManager* sm)
+{
+ try
+ {
+ // Get the name of the interpolant from the symbol manager
+ d_name = sm->getLastSynthName();
+ d_resultStatus = solver->getInterpolantNext(d_result);
+ d_commandStatus = CommandSuccess::instance();
+ }
+ catch (exception& e)
+ {
+ d_commandStatus = new CommandFailure(e.what());
+ }
+}
+
+void GetInterpolNextCommand::printResult(std::ostream& out) const
+{
+ if (!ok())
+ {
+ this->Command::printResult(out);
+ }
+ else
+ {
+ options::ioutils::Scope scope(out);
+ options::ioutils::applyDagThresh(out, 0);
+ if (d_resultStatus)
+ {
+ out << "(define-fun " << d_name << " () Bool " << d_result << ")"
+ << std::endl;
+ }
+ else
+ {
+ out << "none" << std::endl;
+ }
+ }
+}
+
+Command* GetInterpolNextCommand::clone() const
+{
+ GetInterpolNextCommand* c = new GetInterpolNextCommand;
+ c->d_result = d_result;
+ c->d_resultStatus = d_resultStatus;
+ return c;
+}
+
+std::string GetInterpolNextCommand::getCommandName() const
+{
+ return "get-interpol-next";
+}
+
+void GetInterpolNextCommand::toStream(std::ostream& out,
+ int toDepth,
+ size_t dag,
+ Language language) const
+{
+ Printer::getPrinter(language)->toStreamCmdGetInterpolNext(out);
+}
+
/* -------------------------------------------------------------------------- */
/* class GetAbductCommand */
/* -------------------------------------------------------------------------- */
api::Term d_result;
}; /* class GetInterpolCommand */
+/** The command (get-interpol-next) */
+class CVC5_EXPORT GetInterpolNextCommand : public Command
+{
+ public:
+ GetInterpolNextCommand();
+ /**
+ * Get the result of the query, which is the solution to the interpolation
+ * query.
+ */
+ api::Term getResult() const;
+
+ void invoke(api::Solver* solver, SymbolManager* sm) override;
+ void printResult(std::ostream& out) const override;
+ Command* clone() const override;
+ std::string getCommandName() const override;
+ void toStream(std::ostream& out,
+ int toDepth = -1,
+ size_t dag = 1,
+ Language language = Language::LANG_AUTO) const override;
+
+ protected:
+ /** The name of the interpolation predicate */
+ std::string d_name;
+ /** the return status of the command */
+ bool d_resultStatus;
+ /** the return expression of the command */
+ api::Term d_result;
+};
+
/** The command (get-abduct s B (G)?)
*
* This command asks for an abduct from the current set of assertions and
bool d_resultStatus;
/** the return expression of the command */
api::Term d_result;
-}; /* class GetAbductCommand */
+};
class CVC5_EXPORT GetQuantifierEliminationCommand : public Command
{
InterpolationSolver::~InterpolationSolver() {}
-bool InterpolationSolver::getInterpol(const std::vector<Node>& axioms,
- const Node& conj,
- const TypeNode& grammarType,
- Node& interpol)
+bool InterpolationSolver::getInterpolant(const std::vector<Node>& axioms,
+ const Node& conj,
+ const TypeNode& grammarType,
+ Node& interpol)
{
if (options().smt.produceInterpols == options::ProduceInterpols::NONE)
{
conjn = rewrite(conjn);
std::string name("__internal_interpol");
- quantifiers::SygusInterpol interpolSolver(d_env);
- if (interpolSolver.solveInterpolation(
+ d_subsolver = std::make_unique<quantifiers::SygusInterpol>(d_env);
+ if (d_subsolver->solveInterpolation(
name, axioms, conjn, grammarType, interpol))
{
if (options().smt.checkInterpols)
return false;
}
-bool InterpolationSolver::getInterpol(const std::vector<Node>& axioms,
- const Node& conj,
- Node& interpol)
+bool InterpolationSolver::getInterpolantNext(Node& interpol)
{
- TypeNode grammarType;
- return getInterpol(axioms, conj, grammarType, interpol);
+ // should already have initialized a subsolver, since we are immediately
+ // preceeded by a successful call to get-interpol(-next).
+ Assert(d_subsolver != nullptr);
+ return d_subsolver->solveInterpolationNext(interpol);
}
void InterpolationSolver::checkInterpol(Node interpol,
#include "smt/env_obj.h"
namespace cvc5 {
+
+namespace theory {
+namespace quantifiers {
+class SygusInterpol;
+}
+} // namespace theory
+
namespace smt {
/**
* This method invokes a separate copy of the SMT engine for solving the
* corresponding sygus problem for generating such a solution.
*/
- bool getInterpol(const std::vector<Node>& axioms,
- const Node& conj,
- const TypeNode& grammarType,
- Node& interpol);
+ bool getInterpolant(const std::vector<Node>& axioms,
+ const Node& conj,
+ const TypeNode& grammarType,
+ Node& interpol);
/**
- * Same as above, but without user-provided grammar restrictions. A default
- * grammar is chosen internally using the sygus grammar constructor utility.
+ * Get next interpolant. This can only be called immediately after a
+ * successful call to getInterpolant or getInterpolantNext.
+ *
+ * Returns true if an interpolant was found, and sets interpol to the
+ * interpolant.
+ *
+ * This method reuses the subsolver initialized by the last call to
+ * getInterpolant.
*/
- bool getInterpol(const std::vector<Node>& axioms,
- const Node& conj,
- Node& interpol);
+ bool getInterpolantNext(Node& interpol);
+ private:
/**
* Check that a solution to an interpolation problem is indeed a solution.
*
void checkInterpol(Node interpol,
const std::vector<Node>& easserts,
const Node& conj);
+
+ /** The subsolver */
+ std::unique_ptr<theory::quantifiers::SygusInterpol> d_subsolver;
};
} // namespace smt
*d_asserts, q, doFull, d_isInternalSubsolver);
}
-bool SolverEngine::getInterpol(const Node& conj,
- const TypeNode& grammarType,
- Node& interpol)
+bool SolverEngine::getInterpolant(const Node& conj,
+ const TypeNode& grammarType,
+ Node& interpol)
{
SolverEngineScope smts(this);
finishInit();
std::vector<Node> axioms = getExpandedAssertions();
bool success =
- d_interpolSolver->getInterpol(axioms, conj, grammarType, interpol);
+ d_interpolSolver->getInterpolant(axioms, conj, grammarType, interpol);
// notify the state of whether the get-interpol call was successfuly, which
// impacts the SMT mode.
d_state->notifyGetInterpol(success);
return success;
}
-bool SolverEngine::getInterpol(const Node& conj, Node& interpol)
+bool SolverEngine::getInterpolantNext(Node& interpol)
{
- TypeNode grammarType;
- return getInterpol(conj, grammarType, interpol);
+ SolverEngineScope smts(this);
+ finishInit();
+ if (d_state->getMode() != SmtMode::INTERPOL)
+ {
+ throw RecoverableModalException(
+ "Cannot get-interpol-next unless immediately preceded by a successful "
+ "call to get-interpol(-next).");
+ }
+ bool success = d_interpolSolver->getInterpolantNext(interpol);
+ // notify the state of whether the get-interpolant-next call was successful
+ d_state->notifyGetInterpol(success);
+ return success;
}
bool SolverEngine::getAbduct(const Node& conj,
* This method invokes a separate copy of the SMT engine for solving the
* corresponding sygus problem for generating such a solution.
*/
- bool getInterpol(const Node& conj,
- const TypeNode& grammarType,
- Node& interpol);
+ bool getInterpolant(const Node& conj,
+ const TypeNode& grammarType,
+ Node& interpol);
- /** Same as above, but without user-provided grammar restrictions */
- bool getInterpol(const Node& conj, Node& interpol);
+ /**
+ * Get next interpolant. This can only be called immediately after a
+ * successful call to getInterpolant or getInterpolantNext.
+ *
+ * Returns true if an interpolant was found, and sets interpol to the
+ * interpolant.
+ */
+ bool getInterpolantNext(Node& interpol);
/**
* This method asks this SMT engine to find an abduct with respect to the
createVariables(itpGType.isNull());
TypeNode grammarType = setSynthGrammar(itpGType, axioms, conj);
- Node itp = mkPredicate(name);
- mkSygusConjecture(itp, axioms, conj);
+ d_itp = mkPredicate(name);
+ mkSygusConjecture(d_itp, axioms, conj);
- std::unique_ptr<SolverEngine> subSolver;
- initializeSubsolver(subSolver, d_env);
+ initializeSubsolver(d_subSolver, d_env);
// get the logic
- LogicInfo l = subSolver->getLogicInfo().getUnlockedCopy();
+ LogicInfo l = d_subSolver->getLogicInfo().getUnlockedCopy();
// enable everything needed for sygus
l.enableSygus();
- subSolver->setLogic(l);
+ d_subSolver->setLogic(l);
for (const Node& var : d_vars)
{
- subSolver->declareSygusVar(var);
+ d_subSolver->declareSygusVar(var);
}
std::vector<Node> vars_empty;
- subSolver->declareSynthFun(itp, grammarType, false, vars_empty);
- Trace("sygus-interpol") << "SolverEngine::getInterpol: made conjecture : "
- << d_sygusConj << ", solving for "
- << d_sygusConj[0][0] << std::endl;
- subSolver->assertSygusConstraint(d_sygusConj);
+ d_subSolver->declareSynthFun(d_itp, grammarType, false, vars_empty);
+ Trace("sygus-interpol")
+ << "SygusInterpol::solveInterpolation: made conjecture : " << d_sygusConj
+ << ", solving for " << d_sygusConj[0][0] << std::endl;
+ d_subSolver->assertSygusConstraint(d_sygusConj);
- Trace("sygus-interpol") << " SolverEngine::getInterpol check sat..."
- << std::endl;
- Result r = subSolver->checkSynth();
- Trace("sygus-interpol") << " SolverEngine::getInterpol result: " << r
+ Trace("sygus-interpol")
+ << " SygusInterpol::solveInterpolation check synth..." << std::endl;
+ Result r = d_subSolver->checkSynth();
+ Trace("sygus-interpol") << " SygusInterpol::solveInterpolation result: " << r
<< std::endl;
if (r.asSatisfiabilityResult().isSat() == Result::UNSAT)
{
- return findInterpol(subSolver.get(), interpol, itp);
+ return findInterpol(d_subSolver.get(), interpol, d_itp);
+ }
+ return false;
+}
+
+bool SygusInterpol::solveInterpolationNext(Node& interpol)
+{
+ Trace("sygus-interpol")
+ << " SygusInterpol::solveInterpolationNext check synth..." << std::endl;
+ // invoke the check-synth with isNext = true.
+ Result r = d_subSolver->checkSynth(true);
+ Trace("sygus-interpol") << " SygusInterpol::solveInterpolationNext result: "
+ << r << std::endl;
+ if (r.asSatisfiabilityResult().isSat() == Result::UNSAT)
+ {
+ return findInterpol(d_subSolver.get(), interpol, d_itp);
}
return false;
}
const TypeNode& itpGType,
Node& interpol);
+ /**
+ * Returns the sygus conjecture in interpol corresponding to the interpolation
+ * problem for input problem (F above) given by axioms (Fa above), and conj
+ * (Fc above). And solve the interpolation by sygus. Note that axioms is
+ * expected to be a subset of assertions in SMT-LIB.
+ *
+ * @param name the name for the interpol-to-synthesize.
+ * @param axioms the assertions (Fa above)
+ * @param conj the conjecture (Fc above)
+ * @param itpGType (if non-null) a sygus datatype type that encodes the
+ * grammar that should be used for solutions of the interpolation conjecture.
+ * @interpol the solution to the sygus conjecture.
+ */
+ bool solveInterpolationNext(Node& interpol);
+
private:
/**
* Collects symbols from axioms (axioms) and conjecture (conj), which are
* the sygus conjecture to synthesis for interpolation problem
*/
Node d_sygusConj;
+ /**
+ * The predicate for interpolation in the subsolver, which we pass to
+ * findInterpol above when the solving is successful.
+ */
+ Node d_itp;
+ /** The subsolver to initialize */
+ std::unique_ptr<SolverEngine> d_subSolver;
};
} // namespace quantifiers
regress1/sygus/inv-missed-sol-true.sy
regress1/sygus/inv-unused.sy
regress1/sygus/interpol1.smt2
+ regress1/sygus/interpol1-push-pop.smt2
regress1/sygus/interpol3.smt2
+ regress1/sygus/interpol3-next.smt2
regress1/sygus/interpol_arr1.smt2
regress1/sygus/interpol_arr2.smt2
regress1/sygus/interpol_cosa_1.smt2
--- /dev/null
+; COMMAND-LINE: --produce-interpols=default --sygus-active-gen=enum --check-interpols -i
+; SCRUBBER: grep -v -E '(\(define-fun)'
+; EXIT: 0
+(set-logic NIA)
+(declare-fun x ( ) Int)
+(declare-fun y ( ) Int)
+(declare-fun z ( ) Int)
+(push)
+(assert (= (* 2 x) y))
+(get-interpol A (distinct (+ (* 2 z) 1) y)
+
+; the grammar for the interpol-to-synthesize
+((Start Bool) (StartInt Int))
+(
+(Start Bool ((< StartInt StartInt)))
+(StartInt Int
+(y (+ StartInt StartInt) (div StartInt StartInt) (mod StartInt StartInt) 0 1 2))
+)
+)
+(pop)
+
+(assert (= (* 2 y) x))
+(get-interpol A (distinct (+ (* 2 z) 1) x)
+; the grammar for the interpol-to-synthesize
+((Start Bool) (StartInt Int))
+(
+(Start Bool ((< StartInt StartInt)))
+(StartInt Int
+(x (+ StartInt StartInt) (div StartInt StartInt) (mod StartInt StartInt) 0 1 2))
+)
+)
--- /dev/null
+; COMMAND-LINE: --produce-interpols=default --check-interpols -i
+; SCRUBBER: grep -v -E '(\(define-fun)'
+; EXIT: 0
+(set-logic LIA)
+(declare-fun a () Int)
+(assert (> a 1))
+(get-interpol A (> a 0))
+(get-interpol-next)
ASSERT_TRUE(output.getSort().isBoolean());
}
+TEST_F(TestApiBlackSolver, getInterpolantNext)
+{
+ d_solver.setLogic("QF_LIA");
+ d_solver.setOption("produce-interpols", "default");
+ d_solver.setOption("incremental", "true");
+
+ Sort intSort = d_solver.getIntegerSort();
+ Term zero = d_solver.mkInteger(0);
+ Term x = d_solver.mkConst(intSort, "x");
+ Term y = d_solver.mkConst(intSort, "y");
+ Term z = d_solver.mkConst(intSort, "z");
+ // Assumptions for interpolation: x + y > 0 /\ x < 0
+ d_solver.assertFormula(
+ d_solver.mkTerm(GT, d_solver.mkTerm(PLUS, x, y), zero));
+ d_solver.assertFormula(d_solver.mkTerm(LT, x, zero));
+ // Conjecture for interpolation: y + z > 0 \/ z < 0
+ Term conj =
+ d_solver.mkTerm(OR,
+ d_solver.mkTerm(GT, d_solver.mkTerm(PLUS, y, z), zero),
+ d_solver.mkTerm(LT, z, zero));
+ Term output;
+ d_solver.getInterpolant(conj, output);
+ Term output2;
+ d_solver.getInterpolantNext(output2);
+
+ // We expect the next output to be distinct
+ ASSERT_TRUE(output != output2);
+}
+
TEST_F(TestApiBlackSolver, declarePool)
{
Sort intSort = d_solver.getIntegerSort();
assertTrue(output.getSort().isBoolean());
}
+ @Test void getInterpolantNext() throws CVC5ApiException
+ {
+ d_solver.setLogic("QF_LIA");
+ d_solver.setOption("produce-interpols", "default");
+ d_solver.setOption("incremental", "true");
+
+ Sort intSort = d_solver.getIntegerSort();
+ Term zero = d_solver.mkInteger(0);
+ Term x = d_solver.mkConst(intSort, "x");
+ Term y = d_solver.mkConst(intSort, "y");
+ Term z = d_solver.mkConst(intSort, "z");
+
+ d_solver.assertFormula(d_solver.mkTerm(GT, d_solver.mkTerm(PLUS, x, y), zero));
+ d_solver.assertFormula(d_solver.mkTerm(LT, x, zero));
+ Term conj = d_solver.mkTerm(
+ OR, d_solver.mkTerm(GT, d_solver.mkTerm(PLUS, y, z), zero), d_solver.mkTerm(LT, z, zero));
+ Term output = d_solver.getNullTerm();
+ d_solver.getInterpolant(conj, output);
+ Term output2 = d_solver.getNullTerm();
+ d_solver.getInterpolantNext(output2);
+
+ // We expect the next output to be distinct
+ assertNotEquals(output, output2);
+ }
+
@Test void getOp() throws CVC5ApiException
{
Sort bv32 = d_solver.mkBitVectorSort(32);
projects / cvc5.git / commitdiff