From 8ae907ba487d68f6d07324d144a810eb78dd0250 Mon Sep 17 00:00:00 2001 From: Mathias Preiner Date: Mon, 28 Mar 2022 15:30:19 -0700 Subject: [PATCH] Rename get-interpol to get-interpolant. (#8424) --- src/api/cpp/cvc5.cpp | 12 ++-- src/api/cpp/cvc5.h | 23 +++---- src/api/java/io/github/cvc5/api/Solver.java | 14 ++-- src/api/python/cvc5.pxi | 12 ++-- src/options/smt_options.toml | 18 ++--- src/parser/smt2/Smt2.g | 8 +-- src/printer/printer.cpp | 4 +- src/printer/printer.h | 4 +- src/printer/smt2/smt2_printer.cpp | 4 +- src/printer/smt2/smt2_printer.h | 4 +- src/smt/command.cpp | 65 ++++++++++--------- src/smt/command.h | 16 +++-- src/smt/interpolation_solver.cpp | 8 +-- src/smt/interpolation_solver.h | 4 +- src/smt/set_defaults.cpp | 2 +- src/smt/smt_mode.h | 2 +- src/smt/solver_engine.cpp | 11 ++-- src/smt/solver_engine_state.h | 2 +- .../quantifiers/sygus/sygus_interpol.cpp | 13 ++-- src/theory/quantifiers/sygus/sygus_interpol.h | 4 +- .../regress1/sygus/interpol1-push-pop.smt2 | 6 +- .../regress/cli/regress1/sygus/interpol1.smt2 | 4 +- .../cli/regress1/sygus/interpol3-next.smt2 | 6 +- .../regress/cli/regress1/sygus/interpol3.smt2 | 4 +- .../cli/regress1/sygus/interpol_arr1.smt2 | 4 +- .../cli/regress1/sygus/interpol_arr2.smt2 | 4 +- .../cli/regress1/sygus/interpol_cosa_1.smt2 | 4 +- .../cli/regress1/sygus/interpol_dt.smt2 | 4 +- .../regress1/sygus/interpol_from_pono_1.smt2 | 4 +- .../regress1/sygus/interpol_from_pono_2.smt2 | 4 +- .../regress1/sygus/interpol_from_pono_3.smt2 | 4 +- test/regress/cli/regress3/interpol2.smt2 | 4 +- test/unit/api/cpp/solver_black.cpp | 4 +- test/unit/api/java/SolverTest.java | 4 +- test/unit/api/python/test_solver.py | 4 +- 35 files changed, 148 insertions(+), 146 deletions(-) diff --git a/src/api/cpp/cvc5.cpp b/src/api/cpp/cvc5.cpp index 5b36f4d38..c84bd15d0 100644 --- a/src/api/cpp/cvc5.cpp +++ b/src/api/cpp/cvc5.cpp @@ -7143,9 +7143,9 @@ Term Solver::getInterpolant(const Term& conj) const { CVC5_API_TRY_CATCH_BEGIN; CVC5_API_SOLVER_CHECK_TERM(conj); - CVC5_API_CHECK(d_slv->getOptions().smt.interpols) + CVC5_API_CHECK(d_slv->getOptions().smt.interpolants) << "Cannot get interpolant unless interpolants are enabled (try " - "--produce-interpols)"; + "--produce-interpolants)"; //////// all checks before this line TypeNode nullType; Node result = d_slv->getInterpolant(*conj.d_node, nullType); @@ -7158,9 +7158,9 @@ Term Solver::getInterpolant(const Term& conj, Grammar& grammar) const { CVC5_API_TRY_CATCH_BEGIN; CVC5_API_SOLVER_CHECK_TERM(conj); - CVC5_API_CHECK(d_slv->getOptions().smt.interpols) + CVC5_API_CHECK(d_slv->getOptions().smt.interpolants) << "Cannot get interpolant unless interpolants are enabled (try " - "--produce-interpols)"; + "--produce-interpolants)"; //////// all checks before this line Node result = d_slv->getInterpolant(*conj.d_node, *grammar.resolve().d_type); return Term(this, result); @@ -7171,9 +7171,9 @@ Term Solver::getInterpolant(const Term& conj, Grammar& grammar) const Term Solver::getInterpolantNext() const { CVC5_API_TRY_CATCH_BEGIN; - CVC5_API_CHECK(d_slv->getOptions().smt.interpols) + CVC5_API_CHECK(d_slv->getOptions().smt.interpolants) << "Cannot get interpolant unless interpolants are enabled (try " - "--produce-interpols)"; + "--produce-interpolants)"; CVC5_API_CHECK(d_slv->getOptions().base.incrementalSolving) << "Cannot get next interpolant when not solving incrementally (try " "--incremental)"; diff --git a/src/api/cpp/cvc5.h b/src/api/cpp/cvc5.h index 4e8287fa8..bf785793f 100644 --- a/src/api/cpp/cvc5.h +++ b/src/api/cpp/cvc5.h @@ -4337,12 +4337,11 @@ class CVC5_EXPORT Solver * \verbatim embed:rst:leading-asterisk * .. code:: smtlib * - * (get-interpol ) + * (get-interpolant ) * * Requires option - * :ref:`produce-interpols ` to be set to a - * mode different from `none`. - * \endverbatim + * :ref:`produce-interpolants ` to be set to + * a mode different from `none`. \endverbatim * * @warning This method is experimental and may change in future versions. * @@ -4361,12 +4360,11 @@ class CVC5_EXPORT Solver * \verbatim embed:rst:leading-asterisk * .. code:: smtlib * - * (get-interpol ) + * (get-interpolant ) * * Requires option - * :ref:`produce-interpols ` to be set to a - * mode different from `none`. - * \endverbatim + * :ref:`produce-interpolants ` to be set to + * a mode different from `none`. \endverbatim * * @warning This method is experimental and may change in future versions. * @@ -4380,7 +4378,7 @@ class CVC5_EXPORT Solver /** * 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 + * call to get-interpolant or get-interpolant-next. Is guaranteed to produce a * syntactically different interpolant wrt the last returned interpolant if * successful. * @@ -4389,12 +4387,11 @@ class CVC5_EXPORT Solver * \verbatim embed:rst:leading-asterisk * .. code:: smtlib * - * (get-interpol-next) + * (get-interpolant-next) * * Requires to enable incremental mode, and option - * :ref:`produce-interpols ` to be set to a - * mode different from `none`. - * \endverbatim + * :ref:`produce-interpolants ` to be set to + * a mode different from `none`. \endverbatim * * @warning This method is experimental and may change in future versions. * diff --git a/src/api/java/io/github/cvc5/api/Solver.java b/src/api/java/io/github/cvc5/api/Solver.java index a9c270536..7753e8f33 100644 --- a/src/api/java/io/github/cvc5/api/Solver.java +++ b/src/api/java/io/github/cvc5/api/Solver.java @@ -2199,9 +2199,9 @@ public class Solver implements IPointer, AutoCloseable * Get an interpolant * SMT-LIB: * {@code - * ( get-interpol ) + * ( get-interpolant ) * } - * Requires 'produce-interpols' to be set to a mode different from 'none'. + * Requires 'produce-interpolants' to be set to a mode different from 'none'. * * @apiNote This method is experimental and may change in future versions. * @@ -2222,9 +2222,9 @@ public class Solver implements IPointer, AutoCloseable * Get an interpolant * SMT-LIB: * {@code - * ( get-interpol ) + * ( get-interpolant ) * } - * Requires 'produce-interpols' to be set to a mode different from 'none'. + * Requires 'produce-interpolants' to be set to a mode different from 'none'. * * @apiNote This method is experimental and may change in future versions. * @@ -2244,7 +2244,7 @@ public class Solver implements IPointer, AutoCloseable /** * 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 + * call to get-interpolant or get-interpolant-next. Is guaranteed to produce a * syntactically different interpolant wrt the last returned interpolant if * successful. * @@ -2253,9 +2253,9 @@ public class Solver implements IPointer, AutoCloseable * \verbatim embed:rst:leading-asterisk * .. code:: smtlib * - * (get-interpol-next) + * (get-interpolant-next) * - * Requires to enable incremental mode, and option 'produce-interpols' to be + * Requires to enable incremental mode, and option 'produce-interpolants' to be * set to a mode different from 'none'. * \endverbatim * diff --git a/src/api/python/cvc5.pxi b/src/api/python/cvc5.pxi index afbdb8f26..10d714b92 100644 --- a/src/api/python/cvc5.pxi +++ b/src/api/python/cvc5.pxi @@ -2397,10 +2397,10 @@ cdef class Solver: .. code-block:: smtlib - ( get-interpol ) - ( get-interpol ) + ( get-interpolant ) + ( get-interpolant ) - Requires option :ref:`produce-interpols ` to be set to a mode different from `none`. + Requires option :ref:`produce-interpolants ` to be set to a mode different from `none`. Supports the following variants: @@ -2428,7 +2428,7 @@ cdef class Solver: def getInterpolantNext(self): """ Get the next interpolant. Can only be called immediately after - a succesful call to get-interpol or get-interpol-next. + a succesful call to get-interpolant or get-interpolant-next. Is guaranteed to produce a syntactically different interpolant wrt the last returned interpolant if successful. @@ -2436,10 +2436,10 @@ cdef class Solver: .. code-block:: smtlib - ( get-interpol-next ) + ( get-interpolant-next ) Requires to enable incremental mode, and - option :ref:`produce-interpols ` to be set to a mode different from `none`. + option :ref:`produce-interpolants ` to be set to a mode different from `none`. .. warning:: This method is experimental and may change in future versions. diff --git a/src/options/smt_options.toml b/src/options/smt_options.toml index 28b72a168..9aebabde6 100644 --- a/src/options/smt_options.toml +++ b/src/options/smt_options.toml @@ -425,20 +425,20 @@ name = "SMT Layer" help = "attempt to solve a pure real satisfiable problem as an integer problem (for non-linear)" [[option]] - name = "interpols" + name = "interpolants" category = "regular" - long = "produce-interpols" + long = "produce-interpolants" type = "bool" default = "false" help = "turn on interpolation generation." [[option]] - name = "interpolsMode" + name = "interpolantsMode" category = "regular" - long = "interpols-mode=MODE" - type = "InterpolsMode" + long = "interpolants-mode=MODE" + type = "InterpolantsMode" default = "DEFAULT" - help = "choose interpolants production mode, see --interpols-mode=help" + help = "choose interpolants production mode, see --interpolants-mode=help" help_mode = "Interpolants grammar mode" [[option.mode.DEFAULT]] name = "default" @@ -465,12 +465,12 @@ name = "SMT Layer" help = "support the get-abduct command" [[option]] - name = "checkInterpols" + name = "checkInterpolants" category = "regular" - long = "check-interpols" + long = "check-interpolants" type = "bool" default = "false" - help = "checks whether produced solutions to get-interpol are correct" + help = "checks whether produced solutions to get-interpolant are correct" [[option]] name = "checkAbducts" diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g index e0caa77e7..ee95bb080 100644 --- a/src/parser/smt2/Smt2.g +++ b/src/parser/smt2/Smt2.g @@ -1023,11 +1023,11 @@ extendedCommand[std::unique_ptr* cmd] sygusGrammar[g, terms, name] )? { - cmd->reset(new GetInterpolCommand(name, e, g)); + cmd->reset(new GetInterpolantCommand(name, e, g)); } | GET_INTERPOL_NEXT_TOK { PARSER_STATE->checkThatLogicIsSet(); - cmd->reset(new GetInterpolNextCommand); + cmd->reset(new GetInterpolantNextCommand); } | DECLARE_HEAP LPAREN_TOK sortSymbol[t, CHECK_DECLARED] @@ -2251,8 +2251,8 @@ GET_QE_TOK : 'get-qe'; GET_QE_DISJUNCT_TOK : 'get-qe-disjunct'; GET_ABDUCT_TOK : 'get-abduct'; GET_ABDUCT_NEXT_TOK : 'get-abduct-next'; -GET_INTERPOL_TOK : 'get-interpol'; -GET_INTERPOL_NEXT_TOK : 'get-interpol-next'; +GET_INTERPOL_TOK : 'get-interpolant'; +GET_INTERPOL_NEXT_TOK : 'get-interpolant-next'; DECLARE_HEAP : 'declare-heap'; DECLARE_POOL : 'declare-pool'; diff --git a/src/printer/printer.cpp b/src/printer/printer.cpp index f3909ae3f..f543f1be7 100644 --- a/src/printer/printer.cpp +++ b/src/printer/printer.cpp @@ -402,12 +402,12 @@ void Printer::toStreamCmdGetInterpol(std::ostream& out, Node conj, TypeNode sygusType) const { - printUnknownCommand(out, "get-interpol"); + printUnknownCommand(out, "get-interpolant"); } void Printer::toStreamCmdGetInterpolNext(std::ostream& out) const { - printUnknownCommand(out, "get-interpol-next"); + printUnknownCommand(out, "get-interpolant-next"); } void Printer::toStreamCmdGetAbduct(std::ostream& out, diff --git a/src/printer/printer.h b/src/printer/printer.h index 33824d42d..c5dd5ddc2 100644 --- a/src/printer/printer.h +++ b/src/printer/printer.h @@ -194,13 +194,13 @@ class Printer /** Print get-instantiations command */ void toStreamCmdGetInstantiations(std::ostream& out) const; - /** Print get-interpol command */ + /** Print get-interpolant command */ virtual void toStreamCmdGetInterpol(std::ostream& out, const std::string& name, Node conj, TypeNode sygusType) const; - /** Print get-interpol-next command */ + /** Print get-interpolant-next command */ virtual void toStreamCmdGetInterpolNext(std::ostream& out) const; /** Print get-abduct command */ diff --git a/src/printer/smt2/smt2_printer.cpp b/src/printer/smt2/smt2_printer.cpp index 616c51bab..7145471dd 100644 --- a/src/printer/smt2/smt2_printer.cpp +++ b/src/printer/smt2/smt2_printer.cpp @@ -2003,7 +2003,7 @@ void Smt2Printer::toStreamCmdGetInterpol(std::ostream& out, Node conj, TypeNode sygusType) const { - out << "(get-interpol " << cvc5::quoteSymbol(name) << ' ' << conj; + out << "(get-interpolant " << cvc5::quoteSymbol(name) << ' ' << conj; if (!sygusType.isNull()) { out << ' ' << sygusGrammarString(sygusType); @@ -2013,7 +2013,7 @@ void Smt2Printer::toStreamCmdGetInterpol(std::ostream& out, void Smt2Printer::toStreamCmdGetInterpolNext(std::ostream& out) const { - out << "(get-interpol-next)" << std::endl; + out << "(get-interpolant-next)" << std::endl; } void Smt2Printer::toStreamCmdGetAbduct(std::ostream& out, diff --git a/src/printer/smt2/smt2_printer.h b/src/printer/smt2/smt2_printer.h index 6f78f9668..ec403fe00 100644 --- a/src/printer/smt2/smt2_printer.h +++ b/src/printer/smt2/smt2_printer.h @@ -168,13 +168,13 @@ class Smt2Printer : public cvc5::Printer /** Print get-proof command */ void toStreamCmdGetProof(std::ostream& out) const override; - /** Print get-interpol command */ + /** Print get-interpolant command */ void toStreamCmdGetInterpol(std::ostream& out, const std::string& name, Node conj, TypeNode sygusType) const override; - /** Print get-interpol-next command */ + /** Print get-interpolant-next command */ void toStreamCmdGetInterpolNext(std::ostream& out) const override; /** Print get-abduct command */ diff --git a/src/smt/command.cpp b/src/smt/command.cpp index f7772dab6..b8f7fac8d 100644 --- a/src/smt/command.cpp +++ b/src/smt/command.cpp @@ -1897,32 +1897,33 @@ void GetInstantiationsCommand::toStream(std::ostream& out, /* class GetInterpolCommand */ /* -------------------------------------------------------------------------- */ -GetInterpolCommand::GetInterpolCommand(const std::string& name, api::Term conj) +GetInterpolantCommand::GetInterpolantCommand(const std::string& name, + api::Term conj) : d_name(name), d_conj(conj), d_sygus_grammar(nullptr) { } -GetInterpolCommand::GetInterpolCommand(const std::string& name, - api::Term conj, - api::Grammar* g) +GetInterpolantCommand::GetInterpolantCommand(const std::string& name, + api::Term conj, + api::Grammar* g) : d_name(name), d_conj(conj), d_sygus_grammar(g) { } -api::Term GetInterpolCommand::getConjecture() const { return d_conj; } +api::Term GetInterpolantCommand::getConjecture() const { return d_conj; } -const api::Grammar* GetInterpolCommand::getGrammar() const +const api::Grammar* GetInterpolantCommand::getGrammar() const { return d_sygus_grammar; } -api::Term GetInterpolCommand::getResult() const { return d_result; } +api::Term GetInterpolantCommand::getResult() const { return d_result; } -void GetInterpolCommand::invoke(api::Solver* solver, SymbolManager* sm) +void GetInterpolantCommand::invoke(api::Solver* solver, SymbolManager* sm) { try { - // we must remember the name of the interpolant, in case get-interpol-next - // is called later. + // we must remember the name of the interpolant, in case + // get-interpolant-next is called later. sm->setLastSynthName(d_name); if (d_sygus_grammar == nullptr) { @@ -1940,7 +1941,7 @@ void GetInterpolCommand::invoke(api::Solver* solver, SymbolManager* sm) } } -void GetInterpolCommand::printResult(std::ostream& out) const +void GetInterpolantCommand::printResult(std::ostream& out) const { if (!ok()) { @@ -1962,23 +1963,23 @@ void GetInterpolCommand::printResult(std::ostream& out) const } } -Command* GetInterpolCommand::clone() const +Command* GetInterpolantCommand::clone() const { - GetInterpolCommand* c = - new GetInterpolCommand(d_name, d_conj, d_sygus_grammar); + GetInterpolantCommand* c = + new GetInterpolantCommand(d_name, d_conj, d_sygus_grammar); c->d_result = d_result; return c; } -std::string GetInterpolCommand::getCommandName() const +std::string GetInterpolantCommand::getCommandName() const { - return "get-interpol"; + return "get-interpolant"; } -void GetInterpolCommand::toStream(std::ostream& out, - int toDepth, - size_t dag, - Language language) const +void GetInterpolantCommand::toStream(std::ostream& out, + int toDepth, + size_t dag, + Language language) const { Printer::getPrinter(language)->toStreamCmdGetInterpol( out, d_name, termToNode(d_conj), grammarToTypeNode(d_sygus_grammar)); @@ -1988,11 +1989,11 @@ void GetInterpolCommand::toStream(std::ostream& out, /* class GetInterpolNextCommand */ /* -------------------------------------------------------------------------- */ -GetInterpolNextCommand::GetInterpolNextCommand() {} +GetInterpolantNextCommand::GetInterpolantNextCommand() {} -api::Term GetInterpolNextCommand::getResult() const { return d_result; } +api::Term GetInterpolantNextCommand::getResult() const { return d_result; } -void GetInterpolNextCommand::invoke(api::Solver* solver, SymbolManager* sm) +void GetInterpolantNextCommand::invoke(api::Solver* solver, SymbolManager* sm) { try { @@ -2007,7 +2008,7 @@ void GetInterpolNextCommand::invoke(api::Solver* solver, SymbolManager* sm) } } -void GetInterpolNextCommand::printResult(std::ostream& out) const +void GetInterpolantNextCommand::printResult(std::ostream& out) const { if (!ok()) { @@ -2029,22 +2030,22 @@ void GetInterpolNextCommand::printResult(std::ostream& out) const } } -Command* GetInterpolNextCommand::clone() const +Command* GetInterpolantNextCommand::clone() const { - GetInterpolNextCommand* c = new GetInterpolNextCommand; + GetInterpolantNextCommand* c = new GetInterpolantNextCommand; c->d_result = d_result; return c; } -std::string GetInterpolNextCommand::getCommandName() const +std::string GetInterpolantNextCommand::getCommandName() const { - return "get-interpol-next"; + return "get-interpolant-next"; } -void GetInterpolNextCommand::toStream(std::ostream& out, - int toDepth, - size_t dag, - Language language) const +void GetInterpolantNextCommand::toStream(std::ostream& out, + int toDepth, + size_t dag, + Language language) const { Printer::getPrinter(language)->toStreamCmdGetInterpolNext(out); } diff --git a/src/smt/command.h b/src/smt/command.h index 3e4997878..66877f425 100644 --- a/src/smt/command.h +++ b/src/smt/command.h @@ -1012,7 +1012,7 @@ class CVC5_EXPORT GetInstantiationsCommand : public Command api::Solver* d_solver; }; /* class GetInstantiationsCommand */ -/** The command (get-interpol s B (G)?) +/** The command (get-interpolant s B (G)?) * * This command asks for an interpolant from the current set of assertions and * conjecture (goal) B. @@ -1021,12 +1021,14 @@ class CVC5_EXPORT GetInstantiationsCommand : public Command * find a predicate P, then the output response of this command is: (define-fun * s () Bool P) */ -class CVC5_EXPORT GetInterpolCommand : public Command +class CVC5_EXPORT GetInterpolantCommand : public Command { public: - GetInterpolCommand(const std::string& name, api::Term conj); + GetInterpolantCommand(const std::string& name, api::Term conj); /** The argument g is the grammar of the interpolation query */ - GetInterpolCommand(const std::string& name, api::Term conj, api::Grammar* g); + GetInterpolantCommand(const std::string& name, + api::Term conj, + api::Grammar* g); /** Get the conjecture of the interpolation query */ api::Term getConjecture() const; @@ -1056,11 +1058,11 @@ class CVC5_EXPORT GetInterpolCommand : public Command api::Term d_result; }; /* class GetInterpolCommand */ -/** The command (get-interpol-next) */ -class CVC5_EXPORT GetInterpolNextCommand : public Command +/** The command (get-interpolant-next) */ +class CVC5_EXPORT GetInterpolantNextCommand : public Command { public: - GetInterpolNextCommand(); + GetInterpolantNextCommand(); /** * Get the result of the query, which is the solution to the interpolation * query. diff --git a/src/smt/interpolation_solver.cpp b/src/smt/interpolation_solver.cpp index 549d4f28b..e7589ff89 100644 --- a/src/smt/interpolation_solver.cpp +++ b/src/smt/interpolation_solver.cpp @@ -41,10 +41,10 @@ bool InterpolationSolver::getInterpolant(const std::vector& axioms, const TypeNode& grammarType, Node& interpol) { - if (!options().smt.interpols) + if (!options().smt.interpolants) { const char* msg = - "Cannot get interpolation when produce-interpols options is off."; + "Cannot get interpolation when produce-interpolants options is off."; throw ModalException(msg); } Trace("sygus-interpol") << "SolverEngine::getInterpol: conjecture " << conj @@ -58,7 +58,7 @@ bool InterpolationSolver::getInterpolant(const std::vector& axioms, if (d_subsolver->solveInterpolation( name, axioms, conjn, grammarType, interpol)) { - if (options().smt.checkInterpols) + if (options().smt.checkInterpolants) { checkInterpol(interpol, axioms, conj); } @@ -70,7 +70,7 @@ bool InterpolationSolver::getInterpolant(const std::vector& axioms, bool InterpolationSolver::getInterpolantNext(Node& interpol) { // should already have initialized a subsolver, since we are immediately - // preceeded by a successful call to get-interpol(-next). + // preceeded by a successful call to get-interpolant(-next). Assert(d_subsolver != nullptr); return d_subsolver->solveInterpolationNext(interpol); } diff --git a/src/smt/interpolation_solver.h b/src/smt/interpolation_solver.h index d1f1c7fd8..f41cea180 100644 --- a/src/smt/interpolation_solver.h +++ b/src/smt/interpolation_solver.h @@ -35,8 +35,8 @@ namespace smt { /** * A solver for interpolation queries. * - * This class is responsible for responding to get-interpol commands. It spawns - * a subsolver SolverEngine for a sygus conjecture that captures the + * This class is responsible for responding to get-interpolant commands. It + * spawns a subsolver SolverEngine for a sygus conjecture that captures the * interpolation query, and implements supporting utility methods such as * checkInterpol. */ diff --git a/src/smt/set_defaults.cpp b/src/smt/set_defaults.cpp index 4b7e70b4a..9f5e7cbe2 100644 --- a/src/smt/set_defaults.cpp +++ b/src/smt/set_defaults.cpp @@ -856,7 +856,7 @@ bool SetDefaults::isSygus(const Options& opts) const } if (!d_isInternalSubsolver) { - if (opts.smt.produceAbducts || opts.smt.interpols + if (opts.smt.produceAbducts || opts.smt.interpolants || opts.quantifiers.sygusInference || opts.quantifiers.sygusRewSynthInput) { diff --git a/src/smt/smt_mode.h b/src/smt/smt_mode.h index 098bf1cb7..8937c798c 100644 --- a/src/smt/smt_mode.h +++ b/src/smt/smt_mode.h @@ -41,7 +41,7 @@ enum class SmtMode UNSAT, // immediately after a successful call to get-abduct ABDUCT, - // immediately after a successful call to get-interpol + // immediately after a successful call to get-interpolant INTERPOL, // immediately after a successful call to check-synth or check-synth-next SYNTH diff --git a/src/smt/solver_engine.cpp b/src/smt/solver_engine.cpp index 5a27454b7..f1f98c741 100644 --- a/src/smt/solver_engine.cpp +++ b/src/smt/solver_engine.cpp @@ -220,7 +220,7 @@ void SolverEngine::finishInit() { d_abductSolver.reset(new AbductionSolver(*d_env.get())); } - if (d_env->getOptions().smt.interpols) + if (d_env->getOptions().smt.interpolants) { d_interpolSolver.reset(new InterpolationSolver(*d_env)); } @@ -1643,7 +1643,7 @@ Node SolverEngine::getInterpolant(const Node& conj, const TypeNode& grammarType) Node interpol; bool success = d_interpolSolver->getInterpolant(axioms, conj, grammarType, interpol); - // notify the state of whether the get-interpol call was successfuly, which + // notify the state of whether the get-interpolant call was successfuly, which // impacts the SMT mode. d_state->notifyGetInterpol(success); Assert(success == !interpol.isNull()); @@ -1657,12 +1657,13 @@ Node SolverEngine::getInterpolantNext() if (d_state->getMode() != SmtMode::INTERPOL) { throw RecoverableModalException( - "Cannot get-interpol-next unless immediately preceded by a successful " - "call to get-interpol(-next)."); + "Cannot get-interpolant-next unless immediately preceded by a " + "successful " + "call to get-interpolant(-next)."); } Node interpol; bool success = d_interpolSolver->getInterpolantNext(interpol); - // notify the state of whether the get-interpolant-next call was successful + // notify the state of whether the get-interpolantant-next call was successful d_state->notifyGetInterpol(success); Assert(success == !interpol.isNull()); return interpol; diff --git a/src/smt/solver_engine_state.h b/src/smt/solver_engine_state.h index ac1a25e70..fe638181e 100644 --- a/src/smt/solver_engine_state.h +++ b/src/smt/solver_engine_state.h @@ -108,7 +108,7 @@ class SolverEngineState : protected EnvObj /** * Notify that we finished an interpolation query, where success is whether * the command was successful. This is managed independently of the above - * calls for notifying check-sat. In other words, if a get-interpol command + * calls for notifying check-sat. In other words, if a get-interpolant command * is issued to an SolverEngine, it may use a satisfiability call (if desired) * to solve the interpolation query. This method is called *in addition* to * the above calls to notifyCheckSat / notifyCheckSatResult in this case. diff --git a/src/theory/quantifiers/sygus/sygus_interpol.cpp b/src/theory/quantifiers/sygus/sygus_interpol.cpp index cfd49f97b..0d9aecf57 100644 --- a/src/theory/quantifiers/sygus/sygus_interpol.cpp +++ b/src/theory/quantifiers/sygus/sygus_interpol.cpp @@ -99,21 +99,22 @@ void SygusInterpol::getIncludeCons( std::map>& result) { NodeManager* nm = NodeManager::currentNM(); - Assert(options().smt.interpols); + Assert(options().smt.interpolants); // ASSUMPTIONS - if (options().smt.interpolsMode == options::InterpolsMode::ASSUMPTIONS) + if (options().smt.interpolantsMode == options::InterpolantsMode::ASSUMPTIONS) { Node tmpAssumptions = (axioms.size() == 1 ? axioms[0] : nm->mkNode(kind::AND, axioms)); expr::getOperatorsMap(tmpAssumptions, result); } // CONJECTURE - else if (options().smt.interpolsMode == options::InterpolsMode::CONJECTURE) + else if (options().smt.interpolantsMode + == options::InterpolantsMode::CONJECTURE) { expr::getOperatorsMap(conj, result); } // SHARED - else if (options().smt.interpolsMode == options::InterpolsMode::SHARED) + else if (options().smt.interpolantsMode == options::InterpolantsMode::SHARED) { // Get operators from axioms std::map> include_cons_axioms; @@ -153,7 +154,7 @@ void SygusInterpol::getIncludeCons( } } // ALL - else if (options().smt.interpolsMode == options::InterpolsMode::ALL) + else if (options().smt.interpolantsMode == options::InterpolantsMode::ALL) { Node tmpAssumptions = (axioms.size() == 1 ? axioms[0] : nm->mkNode(kind::AND, axioms)); @@ -274,7 +275,7 @@ bool SygusInterpol::findInterpol(SolverEngine* subSolver, Trace("sygus-interpol") << "SolverEngine::getInterpol: could not find solution!" << std::endl; throw RecoverableModalException( - "Could not find solution for get-interpol."); + "Could not find solution for get-interpolant."); return false; } Trace("sygus-interpol") << "SolverEngine::getInterpol: solution is " diff --git a/src/theory/quantifiers/sygus/sygus_interpol.h b/src/theory/quantifiers/sygus/sygus_interpol.h index 604e7435f..78c7da61d 100644 --- a/src/theory/quantifiers/sygus/sygus_interpol.h +++ b/src/theory/quantifiers/sygus/sygus_interpol.h @@ -32,7 +32,7 @@ class SolverEngine; namespace theory { namespace quantifiers { /** - * This is an utility for the SMT-LIB command (get-interpol ). + * This is an utility for the SMT-LIB command (get-interpolant ). * The utility turns a set of quantifier-free assertions into a sygus * conjecture that encodes an interpolation problem, and then solve the * interpolation problem by synthesizing it. In detail, if our input formula is @@ -48,7 +48,7 @@ namespace quantifiers { * * This class uses a fresh copy of the SMT engine which is used for solving the * interpolation problem. In particular, consider the input: (assert A) - * (get-interpol s B) + * (get-interpolant s B) * In the copy of the SMT engine where these commands are issued, we maintain * A in the assertion stack. In solving the interpolation problem, we will * need to call a SMT engine solver with a different assertion stack, which is diff --git a/test/regress/cli/regress1/sygus/interpol1-push-pop.smt2 b/test/regress/cli/regress1/sygus/interpol1-push-pop.smt2 index 120683519..53a25ad12 100644 --- a/test/regress/cli/regress1/sygus/interpol1-push-pop.smt2 +++ b/test/regress/cli/regress1/sygus/interpol1-push-pop.smt2 @@ -1,4 +1,4 @@ -; COMMAND-LINE: --produce-interpols --interpols-mode=default --sygus-enum=fast --check-interpols -i +; COMMAND-LINE: --produce-interpolants --interpolants-mode=default --sygus-enum=fast --check-interpolants -i ; SCRUBBER: grep -v -E '(\(define-fun)' ; EXIT: 0 (set-logic NIA) @@ -7,7 +7,7 @@ (declare-fun z ( ) Int) (push) (assert (= (* 2 x) y)) -(get-interpol A (distinct (+ (* 2 z) 1) y) +(get-interpolant A (distinct (+ (* 2 z) 1) y) ; the grammar for the interpol-to-synthesize ((Start Bool) (StartInt Int)) @@ -20,7 +20,7 @@ (pop) (assert (= (* 2 y) x)) -(get-interpol A (distinct (+ (* 2 z) 1) x) +(get-interpolant A (distinct (+ (* 2 z) 1) x) ; the grammar for the interpol-to-synthesize ((Start Bool) (StartInt Int)) ( diff --git a/test/regress/cli/regress1/sygus/interpol1.smt2 b/test/regress/cli/regress1/sygus/interpol1.smt2 index 4597a2592..7e863c145 100644 --- a/test/regress/cli/regress1/sygus/interpol1.smt2 +++ b/test/regress/cli/regress1/sygus/interpol1.smt2 @@ -1,4 +1,4 @@ -; COMMAND-LINE: --produce-interpols --interpols-mode=default --sygus-enum=fast --check-interpols +; COMMAND-LINE: --produce-interpolants --interpolants-mode=default --sygus-enum=fast --check-interpolants ; SCRUBBER: grep -v -E '(\(define-fun)' ; EXIT: 0 (set-logic NIA) @@ -6,7 +6,7 @@ (declare-fun y ( ) Int) (declare-fun z ( ) Int) (assert (= (* 2 x) y)) -(get-interpol A (distinct (+ (* 2 z) 1) y) +(get-interpolant A (distinct (+ (* 2 z) 1) y) ; the grammar for the interpol-to-synthesize ((Start Bool) (StartInt Int)) diff --git a/test/regress/cli/regress1/sygus/interpol3-next.smt2 b/test/regress/cli/regress1/sygus/interpol3-next.smt2 index 3108e08f8..7eab15652 100644 --- a/test/regress/cli/regress1/sygus/interpol3-next.smt2 +++ b/test/regress/cli/regress1/sygus/interpol3-next.smt2 @@ -1,8 +1,8 @@ -; COMMAND-LINE: --produce-interpols --interpols-mode=default --check-interpols -i +; COMMAND-LINE: --produce-interpolants --interpolants-mode=default --check-interpolants -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) +(get-interpolant A (> a 0)) +(get-interpolant-next) diff --git a/test/regress/cli/regress1/sygus/interpol3.smt2 b/test/regress/cli/regress1/sygus/interpol3.smt2 index 293ff545f..6761129a4 100644 --- a/test/regress/cli/regress1/sygus/interpol3.smt2 +++ b/test/regress/cli/regress1/sygus/interpol3.smt2 @@ -1,7 +1,7 @@ -; COMMAND-LINE: --produce-interpols --interpols-mode=default --check-interpols +; COMMAND-LINE: --produce-interpolants --interpolants-mode=default --check-interpolants ; SCRUBBER: grep -v -E '(\(define-fun)' ; EXIT: 0 (set-logic LIA) (declare-fun a () Int) (assert (> a 1)) -(get-interpol A (> a 0)) +(get-interpolant A (> a 0)) diff --git a/test/regress/cli/regress1/sygus/interpol_arr1.smt2 b/test/regress/cli/regress1/sygus/interpol_arr1.smt2 index a15078bdb..27c0370f3 100644 --- a/test/regress/cli/regress1/sygus/interpol_arr1.smt2 +++ b/test/regress/cli/regress1/sygus/interpol_arr1.smt2 @@ -1,8 +1,8 @@ -; COMMAND-LINE: --produce-interpols --interpols-mode=default --sygus-enum=fast --check-interpols +; COMMAND-LINE: --produce-interpolants --interpolants-mode=default --sygus-enum=fast --check-interpolants ; SCRUBBER: grep -v -E '(\(define-fun)' ; EXIT: 0 (set-logic ALL) (declare-fun a () (Array (_ BitVec 4) (_ BitVec 4))) (declare-fun y () (_ BitVec 4)) (assert (= (select a y) (_ bv0 4))) -(get-interpol A (distinct (select a y) (_ bv1 4))) +(get-interpolant A (distinct (select a y) (_ bv1 4))) diff --git a/test/regress/cli/regress1/sygus/interpol_arr2.smt2 b/test/regress/cli/regress1/sygus/interpol_arr2.smt2 index 9bc7846ad..737b73722 100644 --- a/test/regress/cli/regress1/sygus/interpol_arr2.smt2 +++ b/test/regress/cli/regress1/sygus/interpol_arr2.smt2 @@ -1,4 +1,4 @@ -; COMMAND-LINE: --produce-interpols --interpols-mode=default --sygus-enum=fast --check-interpols +; COMMAND-LINE: --produce-interpolants --interpolants-mode=default --sygus-enum=fast --check-interpolants ; SCRUBBER: grep -v -E '(\(define-fun)' ; EXIT: 0 (set-logic ALL) @@ -12,4 +12,4 @@ (assert (and A1 A2 A3 A4 A5)) ;The conjuecture is: 2 <= x+y -(get-interpol A (<= 2 (+ (select arr 2) (select arr 3)))) +(get-interpolant A (<= 2 (+ (select arr 2) (select arr 3)))) diff --git a/test/regress/cli/regress1/sygus/interpol_cosa_1.smt2 b/test/regress/cli/regress1/sygus/interpol_cosa_1.smt2 index 78a441384..400ead7e5 100644 --- a/test/regress/cli/regress1/sygus/interpol_cosa_1.smt2 +++ b/test/regress/cli/regress1/sygus/interpol_cosa_1.smt2 @@ -1,4 +1,4 @@ -; COMMAND-LINE: --produce-interpols --interpols-mode=conjecture --sygus-enum=fast --check-interpols +; COMMAND-LINE: --produce-interpolants --interpolants-mode=conjecture --sygus-enum=fast --check-interpolants ; SCRUBBER: grep -v -E '(\(define-fun)' ; EXIT: 0 (set-logic ALL) @@ -24,4 +24,4 @@ (declare-fun op@2 () (_ BitVec 4)) (declare-fun witness_0@2 () Bool) (assert (and (and (and (and true (= counter@0 (_ bv0 16))) witness_0@0) (= cfg@0 (_ bv1 1))) (and (and (and (and true (= witness_0@1 (not (= (bvand (ite (bvugt counter@0 ((_ zero_extend 15) (_ bv0 1))) (_ bv1 1) (_ bv0 1)) (bvnot (ite (bvugt counter@0 ((_ zero_extend 15) (_ bv0 1))) (bvcomp (ite (not (distinct op@0 (_ bv0 4))) (bvadd a@0 b@0) (bvsub a@0 b@0)) (bvadd a@0 b@0)) input14@0))) (_ bv1 1))))) (= op@1 (ite (= cfg@0 (_ bv1 1)) (_ bv0 4) op@0))) (= counter@1 (bvadd counter@0 ((_ zero_extend 15) (_ bv1 1))))) (= cfg@1 (_ bv0 1))))) -(get-interpol I (not (and (and true (and (and (and (and true (= witness_0@2 (not (= (bvand (ite (bvugt counter@1 ((_ zero_extend 15) (_ bv0 1))) (_ bv1 1) (_ bv0 1)) (bvnot (ite (bvugt counter@1 ((_ zero_extend 15) (_ bv0 1))) (bvcomp (ite (not (distinct op@1 (_ bv0 4))) (bvadd a@1 b@1) (bvsub a@1 b@1)) (bvadd a@1 b@1)) input14@1))) (_ bv1 1))))) (= op@2 (ite (= cfg@1 (_ bv1 1)) (_ bv0 4) op@1))) (= counter@2 (bvadd counter@1 ((_ zero_extend 15) (_ bv1 1))))) (= cfg@2 (_ bv0 1)))) (not witness_0@2)))) +(get-interpolant I (not (and (and true (and (and (and (and true (= witness_0@2 (not (= (bvand (ite (bvugt counter@1 ((_ zero_extend 15) (_ bv0 1))) (_ bv1 1) (_ bv0 1)) (bvnot (ite (bvugt counter@1 ((_ zero_extend 15) (_ bv0 1))) (bvcomp (ite (not (distinct op@1 (_ bv0 4))) (bvadd a@1 b@1) (bvsub a@1 b@1)) (bvadd a@1 b@1)) input14@1))) (_ bv1 1))))) (= op@2 (ite (= cfg@1 (_ bv1 1)) (_ bv0 4) op@1))) (= counter@2 (bvadd counter@1 ((_ zero_extend 15) (_ bv1 1))))) (= cfg@2 (_ bv0 1)))) (not witness_0@2)))) diff --git a/test/regress/cli/regress1/sygus/interpol_dt.smt2 b/test/regress/cli/regress1/sygus/interpol_dt.smt2 index 50ab5749a..1c7a9b702 100644 --- a/test/regress/cli/regress1/sygus/interpol_dt.smt2 +++ b/test/regress/cli/regress1/sygus/interpol_dt.smt2 @@ -1,4 +1,4 @@ -; COMMAND-LINE: --produce-interpols --interpols-mode=default +; COMMAND-LINE: --produce-interpolants --interpolants-mode=default ; SCRUBBER: grep -v -E '(\(define-fun)' ; EXIT: 0 (set-logic ALL) @@ -9,4 +9,4 @@ (assert ((_ is nil) (tail x))) (assert (= (head x) 0)) (assert (= x y)) -(get-interpol A (distinct y nil)) +(get-interpolant A (distinct y nil)) diff --git a/test/regress/cli/regress1/sygus/interpol_from_pono_1.smt2 b/test/regress/cli/regress1/sygus/interpol_from_pono_1.smt2 index 71c9e4a80..eab515471 100644 --- a/test/regress/cli/regress1/sygus/interpol_from_pono_1.smt2 +++ b/test/regress/cli/regress1/sygus/interpol_from_pono_1.smt2 @@ -1,4 +1,4 @@ -; COMMAND-LINE: --produce-interpols --interpols-mode=default --sygus-enum=fast --check-interpols +; COMMAND-LINE: --produce-interpolants --interpolants-mode=default --sygus-enum=fast --check-interpolants ; SCRUBBER: grep -v -E '(\(define-fun)' ; EXIT: 0 (set-logic ALL) @@ -36,4 +36,4 @@ (declare-fun f1@0 () (_ BitVec 1)) (assert (and (and (and (and (and (and (and (and (and (and (and true (= v_c@0 (_ bv0 16))) (= v_x1@0 (_ bv0 16))) (= v_x2@0 (_ bv0 16))) (= a_Q_a1@0 (_ bv0 1))) (= a_R_a1@0 (_ bv0 1))) (= a_S_a1@0 (_ bv0 1))) (= a_Q_a2@0 (_ bv0 1))) (= a_R_a2@0 (_ bv0 1))) (= a_S_a2@0 (_ bv0 1))) (= dve_invalid@0 (_ bv0 1))) (and (and (and (and (and (and (and (and (and (and true (= v_c@1 (bvxor (_ bv1 16) (ite (= f5@0 (_ bv1 1)) v_x2@0 (ite (= f2@0 (_ bv1 1)) v_x1@0 (bvxor (_ bv1 16) v_c@0)))))) (= v_x1@1 (ite (= f1@0 (_ bv1 1)) ((_ extract 15 0) (bvadd (bvashr (concat (bvxor (_ bv1 16) v_c@0) (_ bv0 16)) (_ bv16 32)) (bvashr (concat v_x1@0 (_ bv0 16)) (_ bv16 32)))) (ite (= f0@0 (_ bv1 1)) (bvxor (_ bv1 16) v_c@0) v_x1@0)))) (= v_x2@1 (ite (= f4@0 (_ bv1 1)) ((_ extract 15 0) (bvadd (bvashr (concat (bvxor (_ bv1 16) v_c@0) (_ bv0 16)) (_ bv16 32)) (bvashr (concat v_x2@0 (_ bv0 16)) (_ bv16 32)))) (ite (= f3@0 (_ bv1 1)) (bvxor (_ bv1 16) v_c@0) v_x2@0)))) (= a_Q_a1@1 (bvnot (bvor (bvand (bvnot a_Q_a1@0) (bvnot f0@0)) f2@0)))) (= a_R_a1@1 (bvand (bvor a_R_a1@0 f0@0) (bvnot f1@0)))) (= a_S_a1@1 (bvand (bvor a_S_a1@0 f1@0) (bvnot f2@0)))) (= a_Q_a2@1 (bvnot (bvor (bvand (bvnot a_Q_a2@0) (bvnot f3@0)) f5@0)))) (= a_R_a2@1 (bvand (bvor a_R_a2@0 f3@0) (bvnot f4@0)))) (= a_S_a2@1 (bvand (bvor a_S_a2@0 f4@0) (bvnot f5@0)))) (= dve_invalid@1 (bvnot (bvand (bvand (bvand (bvand (bvand (bvand (bvand (bvand (bvand (bvand (bvor (bvnot f0@0) (bvand (bvnot a_Q_a1@0) (ite (not (bvule (_ bv200 32) (bvashr (concat (bvxor (_ bv1 16) v_c@0) (_ bv0 16)) (_ bv16 32)))) (_ bv1 1) (_ bv0 1)))) (bvor a_R_a1@0 (bvnot f1@0))) (bvor a_S_a1@0 (bvnot f2@0))) (bvor (bvnot f3@0) (bvand (bvnot a_Q_a2@0) (ite (not (bvule (_ bv200 32) (bvashr (concat (bvxor (_ bv1 16) v_c@0) (_ bv0 16)) (_ bv16 32)))) (_ bv1 1) (_ bv0 1))))) (bvor a_R_a2@0 (bvnot f4@0))) (bvor a_S_a2@0 (bvnot f5@0))) (bvor f5@0 (bvor f4@0 (bvor f3@0 (bvor f2@0 (bvor f0@0 f1@0)))))) (bvnot (bvor (bvor (bvor (bvor (bvand f0@0 f1@0) (bvand f2@0 (bvor f0@0 f1@0))) (bvand f3@0 (bvor f2@0 (bvor f0@0 f1@0)))) (bvand f4@0 (bvor f3@0 (bvor f2@0 (bvor f0@0 f1@0))))) (bvand f5@0 (bvor f4@0 (bvor f3@0 (bvor f2@0 (bvor f0@0 f1@0)))))))) (bvand (bvand (bvand (bvnot (bvor (bvand (bvnot a_Q_a1@0) a_R_a1@0) (bvand a_S_a1@0 (bvor (bvnot a_Q_a1@0) a_R_a1@0)))) (bvor a_S_a1@0 (bvor (bvnot a_Q_a1@0) a_R_a1@0))) (bvnot (bvor (bvand (bvnot a_Q_a2@0) a_R_a2@0) (bvand a_S_a2@0 (bvor (bvnot a_Q_a2@0) a_R_a2@0))))) (bvor a_S_a2@0 (bvor (bvnot a_Q_a2@0) a_R_a2@0)))) (bvand (bvand (bvand (bvnot (bvor (bvand (bvand (bvor a_R_a1@0 f0@0) (bvnot f1@0)) (bvor (bvand (bvnot a_Q_a1@0) (bvnot f0@0)) f2@0)) (bvand (bvand (bvor a_S_a1@0 f1@0) (bvnot f2@0)) (bvor (bvand (bvor a_R_a1@0 f0@0) (bvnot f1@0)) (bvor (bvand (bvnot a_Q_a1@0) (bvnot f0@0)) f2@0))))) (bvor (bvand (bvor a_S_a1@0 f1@0) (bvnot f2@0)) (bvor (bvand (bvor a_R_a1@0 f0@0) (bvnot f1@0)) (bvor (bvand (bvnot a_Q_a1@0) (bvnot f0@0)) f2@0)))) (bvnot (bvor (bvand (bvand (bvor a_R_a2@0 f3@0) (bvnot f4@0)) (bvor (bvand (bvnot a_Q_a2@0) (bvnot f3@0)) f5@0)) (bvand (bvand (bvor a_S_a2@0 f4@0) (bvnot f5@0)) (bvor (bvand (bvor a_R_a2@0 f3@0) (bvnot f4@0)) (bvor (bvand (bvnot a_Q_a2@0) (bvnot f3@0)) f5@0)))))) (bvor (bvand (bvor a_S_a2@0 f4@0) (bvnot f5@0)) (bvor (bvand (bvor a_R_a2@0 f3@0) (bvnot f4@0)) (bvor (bvand (bvnot a_Q_a2@0) (bvnot f3@0)) f5@0))))) (bvnot dve_invalid@0))))))) -(get-interpol I (not (and true (not (not (= (bvand (bvnot dve_invalid@1) (bvcomp (_ bv500 32) (bvashr (concat (bvxor (_ bv1 16) v_c@1) (_ bv0 16)) (_ bv16 32)))) (_ bv1 1))))))) +(get-interpolant I (not (and true (not (not (= (bvand (bvnot dve_invalid@1) (bvcomp (_ bv500 32) (bvashr (concat (bvxor (_ bv1 16) v_c@1) (_ bv0 16)) (_ bv16 32)))) (_ bv1 1))))))) diff --git a/test/regress/cli/regress1/sygus/interpol_from_pono_2.smt2 b/test/regress/cli/regress1/sygus/interpol_from_pono_2.smt2 index 89c067a73..a0ed63d57 100644 --- a/test/regress/cli/regress1/sygus/interpol_from_pono_2.smt2 +++ b/test/regress/cli/regress1/sygus/interpol_from_pono_2.smt2 @@ -1,4 +1,4 @@ -; COMMAND-LINE: --produce-interpols --interpols-mode=default --sygus-enum=fast --check-interpols +; COMMAND-LINE: --produce-interpolants --interpolants-mode=default --sygus-enum=fast --check-interpolants ; SCRUBBER: grep -v -E '(\(define-fun)' ; EXIT: 0 (set-logic ALL) @@ -37,5 +37,5 @@ (assert (and (and (and (and (and (and (and (and (and (and (and true (= v_c@0 (_ bv0 16))) (= v_x1@0 (_ bv0 16))) (= v_x2@0 (_ bv0 16))) (= a_Q_a1@0 (_ bv0 1))) (= a_R_a1@0 (_ bv0 1))) (= a_S_a1@0 (_ bv0 1))) (= a_Q_a2@0 (_ bv0 1))) (= a_R_a2@0 (_ bv0 1))) (= a_S_a2@0 (_ bv0 1))) (= dve_invalid@0 (_ bv0 1))) (and (and (and (and (and (and (and (and (and (and true (= v_c@1 (bvxor (_ bv1 16) (ite (= f5@0 (_ bv1 1)) v_x2@0 (ite (= f2@0 (_ bv1 1)) v_x1@0 (bvxor (_ bv1 16) v_c@0)))))) (= v_x1@1 (ite (= f1@0 (_ bv1 1)) ((_ extract 15 0) (bvadd (bvashr (concat (bvxor (_ bv1 16) v_c@0) (_ bv0 16)) (_ bv16 32)) (bvashr (concat v_x1@0 (_ bv0 16)) (_ bv16 32)))) (ite (= f0@0 (_ bv1 1)) (bvxor (_ bv1 16) v_c@0) v_x1@0)))) (= v_x2@1 (ite (= f4@0 (_ bv1 1)) ((_ extract 15 0) (bvadd (bvashr (concat (bvxor (_ bv1 16) v_c@0) (_ bv0 16)) (_ bv16 32)) (bvashr (concat v_x2@0 (_ bv0 16)) (_ bv16 32)))) (ite (= f3@0 (_ bv1 1)) (bvxor (_ bv1 16) v_c@0) v_x2@0)))) (= a_Q_a1@1 (bvnot (bvor (bvand (bvnot a_Q_a1@0) (bvnot f0@0)) f2@0)))) (= a_R_a1@1 (bvand (bvor a_R_a1@0 f0@0) (bvnot f1@0)))) (= a_S_a1@1 (bvand (bvor a_S_a1@0 f1@0) (bvnot f2@0)))) (= a_Q_a2@1 (bvnot (bvor (bvand (bvnot a_Q_a2@0) (bvnot f3@0)) f5@0)))) (= a_R_a2@1 (bvand (bvor a_R_a2@0 f3@0) (bvnot f4@0)))) (= a_S_a2@1 (bvand (bvor a_S_a2@0 f4@0) (bvnot f5@0)))) (= dve_invalid@1 (bvnot (bvand (bvand (bvand (bvand (bvand (bvand (bvand (bvand (bvand (bvand (bvor (bvnot f0@0) (bvand (bvnot a_Q_a1@0) (ite (not (bvule (_ bv200 32) (bvashr (concat (bvxor (_ bv1 16) v_c@0) (_ bv0 16)) (_ bv16 32)))) (_ bv1 1) (_ bv0 1)))) (bvor a_R_a1@0 (bvnot f1@0))) (bvor a_S_a1@0 (bvnot f2@0))) (bvor (bvnot f3@0) (bvand (bvnot a_Q_a2@0) (ite (not (bvule (_ bv200 32) (bvashr (concat (bvxor (_ bv1 16) v_c@0) (_ bv0 16)) (_ bv16 32)))) (_ bv1 1) (_ bv0 1))))) (bvor a_R_a2@0 (bvnot f4@0))) (bvor a_S_a2@0 (bvnot f5@0))) (bvor f5@0 (bvor f4@0 (bvor f3@0 (bvor f2@0 (bvor f0@0 f1@0)))))) (bvnot (bvor (bvor (bvor (bvor (bvand f0@0 f1@0) (bvand f2@0 (bvor f0@0 f1@0))) (bvand f3@0 (bvor f2@0 (bvor f0@0 f1@0)))) (bvand f4@0 (bvor f3@0 (bvor f2@0 (bvor f0@0 f1@0))))) (bvand f5@0 (bvor f4@0 (bvor f3@0 (bvor f2@0 (bvor f0@0 f1@0)))))))) (bvand (bvand (bvand (bvnot (bvor (bvand (bvnot a_Q_a1@0) a_R_a1@0) (bvand a_S_a1@0 (bvor (bvnot a_Q_a1@0) a_R_a1@0)))) (bvor a_S_a1@0 (bvor (bvnot a_Q_a1@0) a_R_a1@0))) (bvnot (bvor (bvand (bvnot a_Q_a2@0) a_R_a2@0) (bvand a_S_a2@0 (bvor (bvnot a_Q_a2@0) a_R_a2@0))))) (bvor a_S_a2@0 (bvor (bvnot a_Q_a2@0) a_R_a2@0)))) (bvand (bvand (bvand (bvnot (bvor (bvand (bvand (bvor a_R_a1@0 f0@0) (bvnot f1@0)) (bvor (bvand (bvnot a_Q_a1@0) (bvnot f0@0)) f2@0)) (bvand (bvand (bvor a_S_a1@0 f1@0) (bvnot f2@0)) (bvor (bvand (bvor a_R_a1@0 f0@0) (bvnot f1@0)) (bvor (bvand (bvnot a_Q_a1@0) (bvnot f0@0)) f2@0))))) (bvor (bvand (bvor a_S_a1@0 f1@0) (bvnot f2@0)) (bvor (bvand (bvor a_R_a1@0 f0@0) (bvnot f1@0)) (bvor (bvand (bvnot a_Q_a1@0) (bvnot f0@0)) f2@0)))) (bvnot (bvor (bvand (bvand (bvor a_R_a2@0 f3@0) (bvnot f4@0)) (bvor (bvand (bvnot a_Q_a2@0) (bvnot f3@0)) f5@0)) (bvand (bvand (bvor a_S_a2@0 f4@0) (bvnot f5@0)) (bvor (bvand (bvor a_R_a2@0 f3@0) (bvnot f4@0)) (bvor (bvand (bvnot a_Q_a2@0) (bvnot f3@0)) f5@0)))))) (bvor (bvand (bvor a_S_a2@0 f4@0) (bvnot f5@0)) (bvor (bvand (bvor a_R_a2@0 f3@0) (bvnot f4@0)) (bvor (bvand (bvnot a_Q_a2@0) (bvnot f3@0)) f5@0))))) (bvnot dve_invalid@0))))))) (assert (and (or (and (and (and (and (and (and (and (and (and (and true (= v_c@0 (_ bv0 16))) (= v_x1@0 (_ bv0 16))) (= v_x2@0 (_ bv0 16))) (= a_Q_a1@0 (_ bv0 1))) (= a_R_a1@0 (_ bv0 1))) (= a_S_a1@0 (_ bv0 1))) (= a_Q_a2@0 (_ bv0 1))) (= a_R_a2@0 (_ bv0 1))) (= a_S_a2@0 (_ bv0 1))) (= dve_invalid@0 (_ bv0 1))) (bvult v_c@0 (_ bv2 16))) (and (and (and (and (and (and (and (and (and (and true (= v_c@1 (bvxor (_ bv1 16) (ite (= f5@0 (_ bv1 1)) v_x2@0 (ite (= f2@0 (_ bv1 1)) v_x1@0 (bvxor (_ bv1 16) v_c@0)))))) (= v_x1@1 (ite (= f1@0 (_ bv1 1)) ((_ extract 15 0) (bvadd (bvashr (concat (bvxor (_ bv1 16) v_c@0) (_ bv0 16)) (_ bv16 32)) (bvashr (concat v_x1@0 (_ bv0 16)) (_ bv16 32)))) (ite (= f0@0 (_ bv1 1)) (bvxor (_ bv1 16) v_c@0) v_x1@0)))) (= v_x2@1 (ite (= f4@0 (_ bv1 1)) ((_ extract 15 0) (bvadd (bvashr (concat (bvxor (_ bv1 16) v_c@0) (_ bv0 16)) (_ bv16 32)) (bvashr (concat v_x2@0 (_ bv0 16)) (_ bv16 32)))) (ite (= f3@0 (_ bv1 1)) (bvxor (_ bv1 16) v_c@0) v_x2@0)))) (= a_Q_a1@1 (bvnot (bvor (bvand (bvnot a_Q_a1@0) (bvnot f0@0)) f2@0)))) (= a_R_a1@1 (bvand (bvor a_R_a1@0 f0@0) (bvnot f1@0)))) (= a_S_a1@1 (bvand (bvor a_S_a1@0 f1@0) (bvnot f2@0)))) (= a_Q_a2@1 (bvnot (bvor (bvand (bvnot a_Q_a2@0) (bvnot f3@0)) f5@0)))) (= a_R_a2@1 (bvand (bvor a_R_a2@0 f3@0) (bvnot f4@0)))) (= a_S_a2@1 (bvand (bvor a_S_a2@0 f4@0) (bvnot f5@0)))) (= dve_invalid@1 (bvnot (bvand (bvand (bvand (bvand (bvand (bvand (bvand (bvand (bvand (bvand (bvor (bvnot f0@0) (bvand (bvnot a_Q_a1@0) (ite (not (bvule (_ bv200 32) (bvashr (concat (bvxor (_ bv1 16) v_c@0) (_ bv0 16)) (_ bv16 32)))) (_ bv1 1) (_ bv0 1)))) (bvor a_R_a1@0 (bvnot f1@0))) (bvor a_S_a1@0 (bvnot f2@0))) (bvor (bvnot f3@0) (bvand (bvnot a_Q_a2@0) (ite (not (bvule (_ bv200 32) (bvashr (concat (bvxor (_ bv1 16) v_c@0) (_ bv0 16)) (_ bv16 32)))) (_ bv1 1) (_ bv0 1))))) (bvor a_R_a2@0 (bvnot f4@0))) (bvor a_S_a2@0 (bvnot f5@0))) (bvor f5@0 (bvor f4@0 (bvor f3@0 (bvor f2@0 (bvor f0@0 f1@0)))))) (bvnot (bvor (bvor (bvor (bvor (bvand f0@0 f1@0) (bvand f2@0 (bvor f0@0 f1@0))) (bvand f3@0 (bvor f2@0 (bvor f0@0 f1@0)))) (bvand f4@0 (bvor f3@0 (bvor f2@0 (bvor f0@0 f1@0))))) (bvand f5@0 (bvor f4@0 (bvor f3@0 (bvor f2@0 (bvor f0@0 f1@0)))))))) (bvand (bvand (bvand (bvnot (bvor (bvand (bvnot a_Q_a1@0) a_R_a1@0) (bvand a_S_a1@0 (bvor (bvnot a_Q_a1@0) a_R_a1@0)))) (bvor a_S_a1@0 (bvor (bvnot a_Q_a1@0) a_R_a1@0))) (bvnot (bvor (bvand (bvnot a_Q_a2@0) a_R_a2@0) (bvand a_S_a2@0 (bvor (bvnot a_Q_a2@0) a_R_a2@0))))) (bvor a_S_a2@0 (bvor (bvnot a_Q_a2@0) a_R_a2@0)))) (bvand (bvand (bvand (bvnot (bvor (bvand (bvand (bvor a_R_a1@0 f0@0) (bvnot f1@0)) (bvor (bvand (bvnot a_Q_a1@0) (bvnot f0@0)) f2@0)) (bvand (bvand (bvor a_S_a1@0 f1@0) (bvnot f2@0)) (bvor (bvand (bvor a_R_a1@0 f0@0) (bvnot f1@0)) (bvor (bvand (bvnot a_Q_a1@0) (bvnot f0@0)) f2@0))))) (bvor (bvand (bvor a_S_a1@0 f1@0) (bvnot f2@0)) (bvor (bvand (bvor a_R_a1@0 f0@0) (bvnot f1@0)) (bvor (bvand (bvnot a_Q_a1@0) (bvnot f0@0)) f2@0)))) (bvnot (bvor (bvand (bvand (bvor a_R_a2@0 f3@0) (bvnot f4@0)) (bvor (bvand (bvnot a_Q_a2@0) (bvnot f3@0)) f5@0)) (bvand (bvand (bvor a_S_a2@0 f4@0) (bvnot f5@0)) (bvor (bvand (bvor a_R_a2@0 f3@0) (bvnot f4@0)) (bvor (bvand (bvnot a_Q_a2@0) (bvnot f3@0)) f5@0)))))) (bvor (bvand (bvor a_S_a2@0 f4@0) (bvnot f5@0)) (bvor (bvand (bvor a_R_a2@0 f3@0) (bvnot f4@0)) (bvor (bvand (bvnot a_Q_a2@0) (bvnot f3@0)) f5@0))))) (bvnot dve_invalid@0))))))) -(get-interpol I (not (and true (not (not (= (bvand (bvnot dve_invalid@1) (bvcomp (_ bv500 32) (bvashr (concat (bvxor (_ bv1 16) v_c@1) (_ bv0 16)) (_ bv16 32)))) (_ bv1 1))))))) +(get-interpolant I (not (and true (not (not (= (bvand (bvnot dve_invalid@1) (bvcomp (_ bv500 32) (bvashr (concat (bvxor (_ bv1 16) v_c@1) (_ bv0 16)) (_ bv16 32)))) (_ bv1 1))))))) diff --git a/test/regress/cli/regress1/sygus/interpol_from_pono_3.smt2 b/test/regress/cli/regress1/sygus/interpol_from_pono_3.smt2 index 37be96f10..bf9265621 100644 --- a/test/regress/cli/regress1/sygus/interpol_from_pono_3.smt2 +++ b/test/regress/cli/regress1/sygus/interpol_from_pono_3.smt2 @@ -1,4 +1,4 @@ -; COMMAND-LINE: --produce-interpols --interpols-mode=default +; COMMAND-LINE: --produce-interpolants --interpolants-mode=default ; SCRUBBER: grep -v -E '(\(define-fun)' ; EXIT: 0 (set-logic ALL) @@ -49,6 +49,6 @@ (declare-fun v_c@2 () (_ BitVec 16)) (assert (and (and (and (and (and (and (and (and (and (and (and true (= v_c@0 (_ bv0 16))) (= v_x1@0 (_ bv0 16))) (= v_x2@0 (_ bv0 16))) (= a_Q_a1@0 (_ bv0 1))) (= a_R_a1@0 (_ bv0 1))) (= a_S_a1@0 (_ bv0 1))) (= a_Q_a2@0 (_ bv0 1))) (= a_R_a2@0 (_ bv0 1))) (= a_S_a2@0 (_ bv0 1))) (= dve_invalid@0 (_ bv0 1))) (and (and (and (and (and (and (and (and (and (and true (= v_c@1 (bvxor (_ bv1 16) (ite (= f5@0 (_ bv1 1)) v_x2@0 (ite (= f2@0 (_ bv1 1)) v_x1@0 (bvxor (_ bv1 16) v_c@0)))))) (= v_x1@1 (ite (= f1@0 (_ bv1 1)) ((_ extract 15 0) (bvadd (bvashr (concat (bvxor (_ bv1 16) v_c@0) (_ bv0 16)) (_ bv16 32)) (bvashr (concat v_x1@0 (_ bv0 16)) (_ bv16 32)))) (ite (= f0@0 (_ bv1 1)) (bvxor (_ bv1 16) v_c@0) v_x1@0)))) (= v_x2@1 (ite (= f4@0 (_ bv1 1)) ((_ extract 15 0) (bvadd (bvashr (concat (bvxor (_ bv1 16) v_c@0) (_ bv0 16)) (_ bv16 32)) (bvashr (concat v_x2@0 (_ bv0 16)) (_ bv16 32)))) (ite (= f3@0 (_ bv1 1)) (bvxor (_ bv1 16) v_c@0) v_x2@0)))) (= a_Q_a1@1 (bvnot (bvor (bvand (bvnot a_Q_a1@0) (bvnot f0@0)) f2@0)))) (= a_R_a1@1 (bvand (bvor a_R_a1@0 f0@0) (bvnot f1@0)))) (= a_S_a1@1 (bvand (bvor a_S_a1@0 f1@0) (bvnot f2@0)))) (= a_Q_a2@1 (bvnot (bvor (bvand (bvnot a_Q_a2@0) (bvnot f3@0)) f5@0)))) (= a_R_a2@1 (bvand (bvor a_R_a2@0 f3@0) (bvnot f4@0)))) (= a_S_a2@1 (bvand (bvor a_S_a2@0 f4@0) (bvnot f5@0)))) (= dve_invalid@1 (bvnot (bvand (bvand (bvand (bvand (bvand (bvand (bvand (bvand (bvand (bvand (bvor (bvnot f0@0) (bvand (bvnot a_Q_a1@0) (ite (not (bvule (_ bv200 32) (bvashr (concat (bvxor (_ bv1 16) v_c@0) (_ bv0 16)) (_ bv16 32)))) (_ bv1 1) (_ bv0 1)))) (bvor a_R_a1@0 (bvnot f1@0))) (bvor a_S_a1@0 (bvnot f2@0))) (bvor (bvnot f3@0) (bvand (bvnot a_Q_a2@0) (ite (not (bvule (_ bv200 32) (bvashr (concat (bvxor (_ bv1 16) v_c@0) (_ bv0 16)) (_ bv16 32)))) (_ bv1 1) (_ bv0 1))))) (bvor a_R_a2@0 (bvnot f4@0))) (bvor a_S_a2@0 (bvnot f5@0))) (bvor f5@0 (bvor f4@0 (bvor f3@0 (bvor f2@0 (bvor f0@0 f1@0)))))) (bvnot (bvor (bvor (bvor (bvor (bvand f0@0 f1@0) (bvand f2@0 (bvor f0@0 f1@0))) (bvand f3@0 (bvor f2@0 (bvor f0@0 f1@0)))) (bvand f4@0 (bvor f3@0 (bvor f2@0 (bvor f0@0 f1@0))))) (bvand f5@0 (bvor f4@0 (bvor f3@0 (bvor f2@0 (bvor f0@0 f1@0)))))))) (bvand (bvand (bvand (bvnot (bvor (bvand (bvnot a_Q_a1@0) a_R_a1@0) (bvand a_S_a1@0 (bvor (bvnot a_Q_a1@0) a_R_a1@0)))) (bvor a_S_a1@0 (bvor (bvnot a_Q_a1@0) a_R_a1@0))) (bvnot (bvor (bvand (bvnot a_Q_a2@0) a_R_a2@0) (bvand a_S_a2@0 (bvor (bvnot a_Q_a2@0) a_R_a2@0))))) (bvor a_S_a2@0 (bvor (bvnot a_Q_a2@0) a_R_a2@0)))) (bvand (bvand (bvand (bvnot (bvor (bvand (bvand (bvor a_R_a1@0 f0@0) (bvnot f1@0)) (bvor (bvand (bvnot a_Q_a1@0) (bvnot f0@0)) f2@0)) (bvand (bvand (bvor a_S_a1@0 f1@0) (bvnot f2@0)) (bvor (bvand (bvor a_R_a1@0 f0@0) (bvnot f1@0)) (bvor (bvand (bvnot a_Q_a1@0) (bvnot f0@0)) f2@0))))) (bvor (bvand (bvor a_S_a1@0 f1@0) (bvnot f2@0)) (bvor (bvand (bvor a_R_a1@0 f0@0) (bvnot f1@0)) (bvor (bvand (bvnot a_Q_a1@0) (bvnot f0@0)) f2@0)))) (bvnot (bvor (bvand (bvand (bvor a_R_a2@0 f3@0) (bvnot f4@0)) (bvor (bvand (bvnot a_Q_a2@0) (bvnot f3@0)) f5@0)) (bvand (bvand (bvor a_S_a2@0 f4@0) (bvnot f5@0)) (bvor (bvand (bvor a_R_a2@0 f3@0) (bvnot f4@0)) (bvor (bvand (bvnot a_Q_a2@0) (bvnot f3@0)) f5@0)))))) (bvor (bvand (bvor a_S_a2@0 f4@0) (bvnot f5@0)) (bvor (bvand (bvor a_R_a2@0 f3@0) (bvnot f4@0)) (bvor (bvand (bvnot a_Q_a2@0) (bvnot f3@0)) f5@0))))) (bvnot dve_invalid@0))))))) -(get-interpol I (not (and (and true (and (and (and (and (and (and (and (and (and (and true (= v_c@2 (bvxor (_ bv1 16) (ite (= f5@1 (_ bv1 1)) v_x2@1 (ite (= f2@1 (_ bv1 1)) v_x1@1 (bvxor (_ bv1 16) v_c@1)))))) (= v_x1@2 (ite (= f1@1 (_ bv1 1)) ((_ extract 15 0) (bvadd (bvashr (concat (bvxor (_ bv1 16) v_c@1) (_ bv0 16)) (_ bv16 32)) (bvashr (concat v_x1@1 (_ bv0 16)) (_ bv16 32)))) (ite (= f0@1 (_ bv1 1)) (bvxor (_ bv1 16) v_c@1) v_x1@1)))) (= v_x2@2 (ite (= f4@1 (_ bv1 1)) ((_ extract 15 0) (bvadd (bvashr (concat (bvxor (_ bv1 16) v_c@1) (_ bv0 16)) (_ bv16 32)) (bvashr (concat v_x2@1 (_ bv0 16)) (_ bv16 32)))) (ite (= f3@1 (_ bv1 1)) (bvxor (_ bv1 16) v_c@1) v_x2@1)))) (= a_Q_a1@2 (bvnot (bvor (bvand (bvnot a_Q_a1@1) (bvnot f0@1)) f2@1)))) (= a_R_a1@2 (bvand (bvor a_R_a1@1 f0@1) (bvnot f1@1)))) (= a_S_a1@2 (bvand (bvor a_S_a1@1 f1@1) (bvnot f2@1)))) (= a_Q_a2@2 (bvnot (bvor (bvand (bvnot a_Q_a2@1) (bvnot f3@1)) f5@1)))) (= a_R_a2@2 (bvand (bvor a_R_a2@1 f3@1) (bvnot f4@1)))) (= a_S_a2@2 (bvand (bvor a_S_a2@1 f4@1) (bvnot f5@1)))) (= dve_invalid@2 (bvnot (bvand (bvand (bvand (bvand (bvand (bvand (bvand (bvand (bvand (bvand (bvor (bvnot f0@1) (bvand (bvnot a_Q_a1@1) (ite (not (bvule (_ bv200 32) (bvashr (concat (bvxor (_ bv1 16) v_c@1) (_ bv0 16)) (_ bv16 32)))) (_ bv1 1) (_ bv0 1)))) (bvor a_R_a1@1 (bvnot f1@1))) (bvor a_S_a1@1 (bvnot f2@1))) (bvor (bvnot f3@1) (bvand (bvnot a_Q_a2@1) (ite (not (bvule (_ bv200 32) (bvashr (concat (bvxor (_ bv1 16) v_c@1) (_ bv0 16)) (_ bv16 32)))) (_ bv1 1) (_ bv0 1))))) (bvor a_R_a2@1 (bvnot f4@1))) (bvor a_S_a2@1 (bvnot f5@1))) (bvor f5@1 (bvor f4@1 (bvor f3@1 (bvor f2@1 (bvor f0@1 f1@1)))))) (bvnot (bvor (bvor (bvor (bvor (bvand f0@1 f1@1) (bvand f2@1 (bvor f0@1 f1@1))) (bvand f3@1 (bvor f2@1 (bvor f0@1 f1@1)))) (bvand f4@1 (bvor f3@1 (bvor f2@1 (bvor f0@1 f1@1))))) (bvand f5@1 (bvor f4@1 (bvor f3@1 (bvor f2@1 (bvor f0@1 f1@1)))))))) (bvand (bvand (bvand (bvnot (bvor (bvand (bvnot a_Q_a1@1) a_R_a1@1) (bvand a_S_a1@1 (bvor (bvnot a_Q_a1@1) a_R_a1@1)))) (bvor a_S_a1@1 (bvor (bvnot a_Q_a1@1) a_R_a1@1))) (bvnot (bvor (bvand (bvnot a_Q_a2@1) a_R_a2@1) (bvand a_S_a2@1 (bvor (bvnot a_Q_a2@1) a_R_a2@1))))) (bvor a_S_a2@1 (bvor (bvnot a_Q_a2@1) a_R_a2@1)))) (bvand (bvand (bvand (bvnot (bvor (bvand (bvand (bvor a_R_a1@1 f0@1) (bvnot f1@1)) (bvor (bvand (bvnot a_Q_a1@1) (bvnot f0@1)) f2@1)) (bvand (bvand (bvor a_S_a1@1 f1@1) (bvnot f2@1)) (bvor (bvand (bvor a_R_a1@1 f0@1) (bvnot f1@1)) (bvor (bvand (bvnot a_Q_a1@1) (bvnot f0@1)) f2@1))))) (bvor (bvand (bvor a_S_a1@1 f1@1) (bvnot f2@1)) (bvor (bvand (bvor a_R_a1@1 f0@1) (bvnot f1@1)) (bvor (bvand (bvnot a_Q_a1@1) (bvnot f0@1)) f2@1)))) (bvnot (bvor (bvand (bvand (bvor a_R_a2@1 f3@1) (bvnot f4@1)) (bvor (bvand (bvnot a_Q_a2@1) (bvnot f3@1)) f5@1)) (bvand (bvand (bvor a_S_a2@1 f4@1) (bvnot f5@1)) (bvor (bvand (bvor a_R_a2@1 f3@1) (bvnot f4@1)) (bvor (bvand (bvnot a_Q_a2@1) (bvnot f3@1)) f5@1)))))) (bvor (bvand (bvor a_S_a2@1 f4@1) (bvnot f5@1)) (bvor (bvand (bvor a_R_a2@1 f3@1) (bvnot f4@1)) (bvor (bvand (bvnot a_Q_a2@1) (bvnot f3@1)) f5@1))))) (bvnot dve_invalid@1)))))) (not (not (= (bvand (bvnot dve_invalid@2) (bvcomp (_ bv500 32) (bvashr (concat (bvxor (_ bv1 16) v_c@2) (_ bv0 16)) (_ bv16 32)))) (_ bv1 1))))))) +(get-interpolant I (not (and (and true (and (and (and (and (and (and (and (and (and (and true (= v_c@2 (bvxor (_ bv1 16) (ite (= f5@1 (_ bv1 1)) v_x2@1 (ite (= f2@1 (_ bv1 1)) v_x1@1 (bvxor (_ bv1 16) v_c@1)))))) (= v_x1@2 (ite (= f1@1 (_ bv1 1)) ((_ extract 15 0) (bvadd (bvashr (concat (bvxor (_ bv1 16) v_c@1) (_ bv0 16)) (_ bv16 32)) (bvashr (concat v_x1@1 (_ bv0 16)) (_ bv16 32)))) (ite (= f0@1 (_ bv1 1)) (bvxor (_ bv1 16) v_c@1) v_x1@1)))) (= v_x2@2 (ite (= f4@1 (_ bv1 1)) ((_ extract 15 0) (bvadd (bvashr (concat (bvxor (_ bv1 16) v_c@1) (_ bv0 16)) (_ bv16 32)) (bvashr (concat v_x2@1 (_ bv0 16)) (_ bv16 32)))) (ite (= f3@1 (_ bv1 1)) (bvxor (_ bv1 16) v_c@1) v_x2@1)))) (= a_Q_a1@2 (bvnot (bvor (bvand (bvnot a_Q_a1@1) (bvnot f0@1)) f2@1)))) (= a_R_a1@2 (bvand (bvor a_R_a1@1 f0@1) (bvnot f1@1)))) (= a_S_a1@2 (bvand (bvor a_S_a1@1 f1@1) (bvnot f2@1)))) (= a_Q_a2@2 (bvnot (bvor (bvand (bvnot a_Q_a2@1) (bvnot f3@1)) f5@1)))) (= a_R_a2@2 (bvand (bvor a_R_a2@1 f3@1) (bvnot f4@1)))) (= a_S_a2@2 (bvand (bvor a_S_a2@1 f4@1) (bvnot f5@1)))) (= dve_invalid@2 (bvnot (bvand (bvand (bvand (bvand (bvand (bvand (bvand (bvand (bvand (bvand (bvor (bvnot f0@1) (bvand (bvnot a_Q_a1@1) (ite (not (bvule (_ bv200 32) (bvashr (concat (bvxor (_ bv1 16) v_c@1) (_ bv0 16)) (_ bv16 32)))) (_ bv1 1) (_ bv0 1)))) (bvor a_R_a1@1 (bvnot f1@1))) (bvor a_S_a1@1 (bvnot f2@1))) (bvor (bvnot f3@1) (bvand (bvnot a_Q_a2@1) (ite (not (bvule (_ bv200 32) (bvashr (concat (bvxor (_ bv1 16) v_c@1) (_ bv0 16)) (_ bv16 32)))) (_ bv1 1) (_ bv0 1))))) (bvor a_R_a2@1 (bvnot f4@1))) (bvor a_S_a2@1 (bvnot f5@1))) (bvor f5@1 (bvor f4@1 (bvor f3@1 (bvor f2@1 (bvor f0@1 f1@1)))))) (bvnot (bvor (bvor (bvor (bvor (bvand f0@1 f1@1) (bvand f2@1 (bvor f0@1 f1@1))) (bvand f3@1 (bvor f2@1 (bvor f0@1 f1@1)))) (bvand f4@1 (bvor f3@1 (bvor f2@1 (bvor f0@1 f1@1))))) (bvand f5@1 (bvor f4@1 (bvor f3@1 (bvor f2@1 (bvor f0@1 f1@1)))))))) (bvand (bvand (bvand (bvnot (bvor (bvand (bvnot a_Q_a1@1) a_R_a1@1) (bvand a_S_a1@1 (bvor (bvnot a_Q_a1@1) a_R_a1@1)))) (bvor a_S_a1@1 (bvor (bvnot a_Q_a1@1) a_R_a1@1))) (bvnot (bvor (bvand (bvnot a_Q_a2@1) a_R_a2@1) (bvand a_S_a2@1 (bvor (bvnot a_Q_a2@1) a_R_a2@1))))) (bvor a_S_a2@1 (bvor (bvnot a_Q_a2@1) a_R_a2@1)))) (bvand (bvand (bvand (bvnot (bvor (bvand (bvand (bvor a_R_a1@1 f0@1) (bvnot f1@1)) (bvor (bvand (bvnot a_Q_a1@1) (bvnot f0@1)) f2@1)) (bvand (bvand (bvor a_S_a1@1 f1@1) (bvnot f2@1)) (bvor (bvand (bvor a_R_a1@1 f0@1) (bvnot f1@1)) (bvor (bvand (bvnot a_Q_a1@1) (bvnot f0@1)) f2@1))))) (bvor (bvand (bvor a_S_a1@1 f1@1) (bvnot f2@1)) (bvor (bvand (bvor a_R_a1@1 f0@1) (bvnot f1@1)) (bvor (bvand (bvnot a_Q_a1@1) (bvnot f0@1)) f2@1)))) (bvnot (bvor (bvand (bvand (bvor a_R_a2@1 f3@1) (bvnot f4@1)) (bvor (bvand (bvnot a_Q_a2@1) (bvnot f3@1)) f5@1)) (bvand (bvand (bvor a_S_a2@1 f4@1) (bvnot f5@1)) (bvor (bvand (bvor a_R_a2@1 f3@1) (bvnot f4@1)) (bvor (bvand (bvnot a_Q_a2@1) (bvnot f3@1)) f5@1)))))) (bvor (bvand (bvor a_S_a2@1 f4@1) (bvnot f5@1)) (bvor (bvand (bvor a_R_a2@1 f3@1) (bvnot f4@1)) (bvor (bvand (bvnot a_Q_a2@1) (bvnot f3@1)) f5@1))))) (bvnot dve_invalid@1)))))) (not (not (= (bvand (bvnot dve_invalid@2) (bvcomp (_ bv500 32) (bvashr (concat (bvxor (_ bv1 16) v_c@2) (_ bv0 16)) (_ bv16 32)))) (_ bv1 1))))))) diff --git a/test/regress/cli/regress3/interpol2.smt2 b/test/regress/cli/regress3/interpol2.smt2 index 7050fbd63..67805b016 100644 --- a/test/regress/cli/regress3/interpol2.smt2 +++ b/test/regress/cli/regress3/interpol2.smt2 @@ -1,4 +1,4 @@ -; COMMAND-LINE: --produce-interpols --interpols-mode=default --sygus-enum=fast --check-interpols +; COMMAND-LINE: --produce-interpolants --interpolants-mode=default --sygus-enum=fast --check-interpolants ; SCRUBBER: grep -v -E '(\(define-fun)' ; EXIT: 0 @@ -28,4 +28,4 @@ (assert (and A1 A2 A3 A4 A5)) ;The conjuecture is: 2 <= x+y -(get-interpol A (<= 2 (+ x y))) +(get-interpolant A (<= 2 (+ x y))) diff --git a/test/unit/api/cpp/solver_black.cpp b/test/unit/api/cpp/solver_black.cpp index 1921cd645..edb9c291a 100644 --- a/test/unit/api/cpp/solver_black.cpp +++ b/test/unit/api/cpp/solver_black.cpp @@ -1402,7 +1402,7 @@ TEST_F(TestApiBlackSolver, getAbductNext) TEST_F(TestApiBlackSolver, getInterpolant) { d_solver.setLogic("QF_LIA"); - d_solver.setOption("produce-interpols", "true"); + d_solver.setOption("produce-interpolants", "true"); d_solver.setOption("incremental", "false"); Sort intSort = d_solver.getIntegerSort(); @@ -1430,7 +1430,7 @@ TEST_F(TestApiBlackSolver, getInterpolant) TEST_F(TestApiBlackSolver, getInterpolantNext) { d_solver.setLogic("QF_LIA"); - d_solver.setOption("produce-interpols", "true"); + d_solver.setOption("produce-interpolants", "true"); d_solver.setOption("incremental", "true"); Sort intSort = d_solver.getIntegerSort(); diff --git a/test/unit/api/java/SolverTest.java b/test/unit/api/java/SolverTest.java index e4b981dfa..c0e4d9d46 100644 --- a/test/unit/api/java/SolverTest.java +++ b/test/unit/api/java/SolverTest.java @@ -1394,7 +1394,7 @@ class SolverTest @Test void getInterpolant() throws CVC5ApiException { d_solver.setLogic("QF_LIA"); - d_solver.setOption("produce-interpols", "true"); + d_solver.setOption("produce-interpolants", "true"); d_solver.setOption("incremental", "false"); Sort intSort = d_solver.getIntegerSort(); @@ -1419,7 +1419,7 @@ class SolverTest @Test void getInterpolantNext() throws CVC5ApiException { d_solver.setLogic("QF_LIA"); - d_solver.setOption("produce-interpols", "true"); + d_solver.setOption("produce-interpolants", "true"); d_solver.setOption("incremental", "true"); Sort intSort = d_solver.getIntegerSort(); diff --git a/test/unit/api/python/test_solver.py b/test/unit/api/python/test_solver.py index baf52b897..f1c69e8cd 100644 --- a/test/unit/api/python/test_solver.py +++ b/test/unit/api/python/test_solver.py @@ -2147,7 +2147,7 @@ def test_get_abduct_next(solver): def test_get_interpolant(solver): solver.setLogic("QF_LIA") - solver.setOption("produce-interpols", "true") + solver.setOption("produce-interpolants", "true") solver.setOption("incremental", "false") intSort = solver.getIntegerSort() @@ -2168,7 +2168,7 @@ def test_get_interpolant(solver): def test_get_interpolant_next(solver): solver.setLogic("QF_LIA") - solver.setOption("produce-interpols", "true") + solver.setOption("produce-interpolants", "true") solver.setOption("incremental", "true") intSort = solver.getIntegerSort() -- 2.30.2