Rename get-interpol to get-interpolant. (#8424)

diff --git a/src/api/cpp/cvc5.cpp b/src/api/cpp/cvc5.cpp
index 5b36f4d388d83281bfd7f70ee1afe75705961ef6..c84bd15d03e8e01ce062bff155ac2abef95fe0bf 100644 (file)
--- 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 4e8287fa888d06aad483479e50b04f21a4731ec1..bf785793f34f50bd687e575e6386167acc82b4cd 100644 (file)
--- 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 <conj>)
+   *     (get-interpolant <conj>)
    *
    * Requires option
-   * :ref:`produce-interpols <lbl-option-produce-interpols>` to be set to a
-   * mode different from `none`.
-   * \endverbatim
+   * :ref:`produce-interpolants <lbl-option-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 <conj> <grammar>)
+   *     (get-interpolant <conj> <grammar>)
    *
    * Requires option
-   * :ref:`produce-interpols <lbl-option-produce-interpols>` to be set to a
-   * mode different from `none`.
-   * \endverbatim
+   * :ref:`produce-interpolants <lbl-option-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 <lbl-option-produce-interpols>` to be set to a
-   * mode different from `none`.
-   * \endverbatim
+   * :ref:`produce-interpolants <lbl-option-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 a9c270536cd8680d4851d62057ac31158433e56a..7753e8f33ced2198ccd9351dc99811a053c6a593 100644 (file)
--- 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 <conj> )
+   * ( get-interpolant <conj> )
    * }
-   * 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 <conj> <g> )
+   * ( get-interpolant <conj> <g> )
    * }
-   * 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 afbdb8f26a72ac8e8604b8735a4586abd99b5e38..10d714b92caa87dc9cfa71dc91df0bfc84cf775c 100644 (file)
--- a/src/api/python/cvc5.pxi
+++ b/src/api/python/cvc5.pxi
@@ -2397,10 +2397,10 @@ cdef class Solver:
 
         .. code-block:: smtlib
 
-            ( get-interpol <conj> )
-            ( get-interpol <conj> <grammar> )
+            ( get-interpolant <conj> )
+            ( get-interpolant <conj> <grammar> )
 
-        Requires option :ref:`produce-interpols <lbl-option-produce-interpols>` to be set to a mode different from `none`.
+        Requires option :ref:`produce-interpolants <lbl-option-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 <lbl-option-produce-interpols>` to be set to a mode different from `none`.
+        option :ref:`produce-interpolants <lbl-option-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 28b72a168fa37ca9d566c75ec4a5e633d9ed20b5..9aebabde618cb97448173147bc432d8952432d4f 100644 (file)
--- 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 e0caa77e7dde0bfe31b18c9962f50fe9184a2af7..ee95bb0801b324a8ab248a2ea4315390e629fe92 100644 (file)
--- a/src/parser/smt2/Smt2.g
+++ b/src/parser/smt2/Smt2.g
@@ -1023,11 +1023,11 @@ extendedCommand[std::unique_ptr<cvc5::Command>* 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 f3909ae3f689f2def7c2b0934d4830a935c8c6dd..f543f1be723cb3013f62c09466a243bc24995c7c 100644 (file)
--- 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 33824d42deb80f3fa30a43dac83dbe73a2bd47cf..c5dd5ddc2608e219134512636a39d2c9cf80bcad 100644 (file)
--- 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 616c51bab1e1ec389f9a0b43da0e352331e64740..7145471dd82e45f99ed370416cadce7f15e72594 100644 (file)
--- 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 6f78f96689cca61f5aa18c1b9f14e1e939046b27..ec403fe001beed7bae29c3ac3c3f184a6bdb2062 100644 (file)
--- 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 f7772dab635c63cef8a2b37f19ff186689ca781e..b8f7fac8d4fd78815728a98dea9d256e7a435c77 100644 (file)
--- 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 3e4997878e0111adbcbd778ffc2b411949676e1c..66877f425357fdc2cf9cf9a54986925bb6385ceb 100644 (file)
--- 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 549d4f28b705bbe698be51f30391de787edb7f13..e7589ff8984161c171e19e59b9225b40c29ebae9 100644 (file)
--- a/src/smt/interpolation_solver.cpp
+++ b/src/smt/interpolation_solver.cpp
@@ -41,10 +41,10 @@ bool InterpolationSolver::getInterpolant(const std::vector<Node>& 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<Node>& 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<Node>& 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 d1f1c7fd885bff70b8da249eecbb61bfb4fb8a89..f41cea180d9b8f50051b19cede63ec79cf3812ab 100644 (file)
--- 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 4b7e70b4a3d4597c4eebdbfb5f4e0b717e9260d3..9f5e7cbe28b0f74af3f725431e23a4ed380e311b 100644 (file)
--- 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 098bf1cb754eeaada9aa10ef30c12f7227e2e449..8937c798ce1caa78fd415c86b0a4f27aba247c2a 100644 (file)
--- 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 5a27454b7c7b5eccd198a789a1274fa296d0c226..f1f98c7413e8a359c2ffe4de1150c0add00c2399 100644 (file)
--- 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 ac1a25e70e6b1d9bfaced014217bc3a11dccbb38..fe638181e41847c352203c2ebdb2cc78f65ae22e 100644 (file)
--- 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 cfd49f97b9cbec8ce73426930e55eb58fe813772..0d9aecf57d1b51be40f80c439fce0ea16ebd0f14 100644 (file)
--- 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<TypeNode, std::unordered_set<Node>>& 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<TypeNode, std::unordered_set<Node>> 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 604e7435fa31a468b79fee427d8990d152fdc8e5..78c7da61d4bbb62fc055e9f3892ce9772db96046 100644 (file)
--- 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 <term>).
+ * This is an utility for the SMT-LIB command (get-interpolant <term>).
  * 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 120683519c2a84f7bc85198e38cb83d8e092c052..53a25ad12e597e466b44cddeb532a34af9aa840a 100644 (file)
--- 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 4597a25921a7a8e4957f9cab379852285a76d745..7e863c145d6db0dac828d48672a2617f87d07a54 100644 (file)
--- 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 3108e08f8017ca12010786e6a85549956d8ce0d8..7eab15652d95e0574daa610466010f8a3ec33116 100644 (file)
--- 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 293ff545f153559fb95539a7e64033ce149695dd..6761129a4982bffb7e4e0d6e73b93a8fe0223d90 100644 (file)
--- 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 a15078bdbf5dc8c9886e542c77bf668ce79d9fd4..27c0370f3a54264dc0bd8083cb3155c14a772266 100644 (file)
--- 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 9bc7846ad4bd0af07a89d9f1954ebdd227825193..737b737223b44f97b0bc64b20e1ab44803f41bae 100644 (file)
--- 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 78a441384b7e37a8cced9011bf71bc3ea8ca2870..400ead7e517e7e7ab455504c06f58178a6098a21 100644 (file)
--- 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 50ab5749a91ea76e61043b3955a8b7136052a254..1c7a9b702cf82a31dc442436a6882e44c5e81be7 100644 (file)
--- 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 71c9e4a800d16838a222742066388c9249ed2c1a..eab515471680acf73b6d00397521ba61c00b8f28 100644 (file)
--- 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 89c067a73143b3c6347c3957dde3241065e529e6..a0ed63d57c1d5035364ec8369713a9c413a4fd9a 100644 (file)
--- 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 37be96f10bc7d34e6caf9949247538c5f014c519..bf9265621c51bd923764688ab3387e5b68f7b935 100644 (file)
--- 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 7050fbd63470430cf5d1c80787e97f83637c15e6..67805b0169eef974adaa938008a0493424779d2f 100644 (file)
--- 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 1921cd645f91a04d7528ccbffb9fc7604623374c..edb9c291ac9b944579dee8b613ba62c559cece5d 100644 (file)
--- 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 e4b981dfa6411a495749a0cd607d5c056e7ad6b2..c0e4d9d46259dd04926e7bf871e9356e2c568ee1 100644 (file)
--- 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 baf52b897097cbc9bcb0787080b1dc6bc1771cbe..f1c69e8cd929fbe48ac3e2b6ccfd5efe5b967455 100644 (file)
--- 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()