Support sygus version 2.1 command assume (#7081)

Adds support for global assumptions in sygus files.

Also guards against cases of declare-const, which should be prohibited in sygus.

diff --git a/src/api/cpp/cvc5.cpp b/src/api/cpp/cvc5.cpp
index 1aa9a740fa452d571c601ffa8092f0a68c5ad651..03c464e08703c5cea1871871c8fed2ae6977519d 100644 (file)
--- a/src/api/cpp/cvc5.cpp
+++ b/src/api/cpp/cvc5.cpp
@@ -7819,7 +7819,21 @@ void Solver::addSygusConstraint(const Term& term) const
       term.d_node->getType() == getNodeManager()->booleanType(), term)
       << "boolean term";
   //////// all checks before this line
-  d_smtEngine->assertSygusConstraint(*term.d_node);
+  d_smtEngine->assertSygusConstraint(*term.d_node, false);
+  ////////
+  CVC5_API_TRY_CATCH_END;
+}
+
+void Solver::addSygusAssume(const Term& term) const
+{
+  NodeManagerScope scope(getNodeManager());
+  CVC5_API_TRY_CATCH_BEGIN;
+  CVC5_API_SOLVER_CHECK_TERM(term);
+  CVC5_API_ARG_CHECK_EXPECTED(
+      term.d_node->getType() == getNodeManager()->booleanType(), term)
+      << "boolean term";
+  //////// all checks before this line
+  d_smtEngine->assertSygusConstraint(*term.d_node, true);
   ////////
   CVC5_API_TRY_CATCH_END;
 }

diff --git a/src/api/cpp/cvc5.h b/src/api/cpp/cvc5.h
index 9324e42091a96cda3e7a34f5ee9c873425984ff9..684b891148496025d6a1f04471c72553d4e70fca 100644 (file)
--- a/src/api/cpp/cvc5.h
+++ b/src/api/cpp/cvc5.h
@@ -4303,6 +4303,16 @@ class CVC5_EXPORT Solver
    */
   void addSygusConstraint(const Term& term) const;
 
+  /**
+   * Add a forumla to the set of Sygus assumptions.
+   * SyGuS v2:
+   * \verbatim
+   *   ( assume <term> )
+   * \endverbatim
+   * @param term the formula to add as an assumption
+   */
+  void addSygusAssume(const Term& term) const;
+
   /**
    * Add a set of Sygus constraints to the current state that correspond to an
    * invariant synthesis problem.

diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g
index 22a042951fb4187d632a7cdfbce4dbacb0107104..2c391169c2c94d5920297a86b2cd84978fdc2e9f 100644 (file)
--- a/src/parser/smt2/Smt2.g
+++ b/src/parser/smt2/Smt2.g
@@ -518,6 +518,7 @@ sygusCommand returns [std::unique_ptr<cvc5::Command> cmd]
   std::vector<std::pair<std::string, cvc5::api::Sort> > sortedVarNames;
   std::vector<cvc5::api::Term> sygusVars;
   std::string name;
+  bool isAssume;
   bool isInv;
   cvc5::api::Grammar* grammar = nullptr;
 }
@@ -568,14 +569,13 @@ sygusCommand returns [std::unique_ptr<cvc5::Command> cmd]
           new SynthFunCommand(name, fun, sygusVars, range, isInv, grammar));
     }
   | /* constraint */
-    CONSTRAINT_TOK {
+    ( CONSTRAINT_TOK { isAssume = false; } | ASSUME_TOK { isAssume = true; } )
+    {
       PARSER_STATE->checkThatLogicIsSet();
-      Debug("parser-sygus") << "Sygus : define sygus funs..." << std::endl;
-      Debug("parser-sygus") << "Sygus : read constraint..." << std::endl;
     }
     term[expr, expr2]
     { Debug("parser-sygus") << "...read constraint " << expr << std::endl;
-      cmd.reset(new SygusConstraintCommand(expr));
+      cmd.reset(new SygusConstraintCommand(expr, isAssume));
     }
   | /* inv-constraint */
     INV_CONSTRAINT_TOK
@@ -784,6 +784,11 @@ smt25Command[std::unique_ptr<cvc5::Command>* cmd]
     { PARSER_STATE->checkUserSymbol(name); }
     sortSymbol[t,CHECK_DECLARED]
     { // allow overloading here
+      if( PARSER_STATE->sygus() )
+      {
+        PARSER_STATE->parseErrorLogic("declare-const is not allowed in sygus "
+                                      "version 2.0");
+      }
       api::Term c =
           PARSER_STATE->bindVar(name, t, false, true);
       cmd->reset(new DeclareFunctionCommand(name, c, t)); }
@@ -2272,6 +2277,7 @@ SYNTH_INV_TOK : { PARSER_STATE->sygus()}?'synth-inv';
 CHECK_SYNTH_TOK : { PARSER_STATE->sygus()}?'check-synth';
 DECLARE_VAR_TOK : { PARSER_STATE->sygus()}?'declare-var';
 CONSTRAINT_TOK : { PARSER_STATE->sygus()}?'constraint';
+ASSUME_TOK : { PARSER_STATE->sygus()}?'assume';
 INV_CONSTRAINT_TOK : { PARSER_STATE->sygus()}?'inv-constraint';
 SET_FEATURE_TOK : { PARSER_STATE->sygus() }? 'set-feature';
 SYGUS_CONSTANT_TOK : { PARSER_STATE->sygus() }? 'Constant';

diff --git a/src/printer/printer.cpp b/src/printer/printer.cpp
index 9bd68e6971f0629990a34c68a260d4e238e20903..01fa7a9fdbd6d9d5d873750ebcc9a672f86fefe7 100644 (file)
--- a/src/printer/printer.cpp
+++ b/src/printer/printer.cpp
@@ -340,6 +340,11 @@ void Printer::toStreamCmdConstraint(std::ostream& out, Node n) const
   printUnknownCommand(out, "constraint");
 }
 
+void Printer::toStreamCmdAssume(std::ostream& out, Node n) const
+{
+  printUnknownCommand(out, "assume");
+}
+
 void Printer::toStreamCmdInvConstraint(
     std::ostream& out, Node inv, Node pre, Node trans, Node post) const
 {

diff --git a/src/printer/printer.h b/src/printer/printer.h
index 5ffe07f775e0ae060f4a4d8682dd3ca653903a52..499a9398fa3c09fa83a8a971c9399d674c653b4a 100644 (file)
--- a/src/printer/printer.h
+++ b/src/printer/printer.h
@@ -156,6 +156,9 @@ class Printer
   /** Print constraint command */
   virtual void toStreamCmdConstraint(std::ostream& out, Node n) const;
 
+  /** Print assume command */
+  virtual void toStreamCmdAssume(std::ostream& out, Node n) const;
+
   /** Print inv-constraint command */
   virtual void toStreamCmdInvConstraint(
       std::ostream& out, Node inv, Node pre, Node trans, Node post) const;

diff --git a/src/printer/smt2/smt2_printer.cpp b/src/printer/smt2/smt2_printer.cpp
index 0d556c1dc46e345248869eac7e239eacfafc9424..07c5b10d819cf292a8bb772641e28ffceae422e2 100644 (file)
--- a/src/printer/smt2/smt2_printer.cpp
+++ b/src/printer/smt2/smt2_printer.cpp
@@ -1877,6 +1877,11 @@ void Smt2Printer::toStreamCmdConstraint(std::ostream& out, Node n) const
   out << "(constraint " << n << ')' << std::endl;
 }
 
+void Smt2Printer::toStreamCmdAssume(std::ostream& out, Node n) const
+{
+  out << "(assume " << n << ')' << std::endl;
+}
+
 void Smt2Printer::toStreamCmdInvConstraint(
     std::ostream& out, Node inv, Node pre, Node trans, Node post) const
 {

diff --git a/src/printer/smt2/smt2_printer.h b/src/printer/smt2/smt2_printer.h
index 729caebf4502d8fae5b50d86d5f6d47aece8f7c2..fd7e0c7ac75fb8503e3633c16ec71d10bd87ea0b 100644 (file)
--- a/src/printer/smt2/smt2_printer.h
+++ b/src/printer/smt2/smt2_printer.h
@@ -124,6 +124,9 @@ class Smt2Printer : public cvc5::Printer
   /** Print constraint command */
   void toStreamCmdConstraint(std::ostream& out, Node n) const override;
 
+  /** Print assume command */
+  void toStreamCmdAssume(std::ostream& out, Node n) const override;
+
   /** Print inv-constraint command */
   void toStreamCmdInvConstraint(std::ostream& out,
                                 Node inv,

diff --git a/src/smt/command.cpp b/src/smt/command.cpp
index adfd2f71d75f3882e0b9ff192824e7f328fe376e..4b04abcb26b2d25a0a57908600f8df3f7bc16947 100644 (file)
--- a/src/smt/command.cpp
+++ b/src/smt/command.cpp
@@ -732,7 +732,9 @@ void SynthFunCommand::toStream(std::ostream& out,
 /* class SygusConstraintCommand */
 /* -------------------------------------------------------------------------- */
 
-SygusConstraintCommand::SygusConstraintCommand(const api::Term& t) : d_term(t)
+SygusConstraintCommand::SygusConstraintCommand(const api::Term& t,
+                                               bool isAssume)
+    : d_term(t), d_isAssume(isAssume)
 {
 }
 
@@ -740,7 +742,14 @@ void SygusConstraintCommand::invoke(api::Solver* solver, SymbolManager* sm)
 {
   try
   {
-    solver->addSygusConstraint(d_term);
+    if (d_isAssume)
+    {
+      solver->addSygusAssume(d_term);
+    }
+    else
+    {
+      solver->addSygusConstraint(d_term);
+    }
     d_commandStatus = CommandSuccess::instance();
   }
   catch (exception& e)
@@ -753,12 +762,12 @@ api::Term SygusConstraintCommand::getTerm() const { return d_term; }
 
 Command* SygusConstraintCommand::clone() const
 {
-  return new SygusConstraintCommand(d_term);
+  return new SygusConstraintCommand(d_term, d_isAssume);
 }
 
 std::string SygusConstraintCommand::getCommandName() const
 {
-  return "constraint";
+  return d_isAssume ? "assume" : "constraint";
 }
 
 void SygusConstraintCommand::toStream(std::ostream& out,
@@ -766,7 +775,15 @@ void SygusConstraintCommand::toStream(std::ostream& out,
                                       size_t dag,
                                       Language language) const
 {
-  Printer::getPrinter(language)->toStreamCmdConstraint(out, termToNode(d_term));
+  if (d_isAssume)
+  {
+    Printer::getPrinter(language)->toStreamCmdAssume(out, termToNode(d_term));
+  }
+  else
+  {
+    Printer::getPrinter(language)->toStreamCmdConstraint(out,
+                                                         termToNode(d_term));
+  }
 }
 
 /* -------------------------------------------------------------------------- */

diff --git a/src/smt/command.h b/src/smt/command.h
index b374a48c965ec20adfa8e006fc17522b3558d5ee..7587aaa636b396b1a3139f03d8dd94fe13dca224 100644 (file)
--- a/src/smt/command.h
+++ b/src/smt/command.h
@@ -765,7 +765,7 @@ class CVC5_EXPORT SynthFunCommand : public DeclarationDefinitionCommand
 class CVC5_EXPORT SygusConstraintCommand : public Command
 {
  public:
-  SygusConstraintCommand(const api::Term& t);
+  SygusConstraintCommand(const api::Term& t, bool isAssume = false);
   /** returns the declared constraint */
   api::Term getTerm() const;
   /** invokes this command
@@ -787,6 +787,8 @@ class CVC5_EXPORT SygusConstraintCommand : public Command
  protected:
   /** the declared constraint */
   api::Term d_term;
+  /** true if this is a sygus assumption */
+  bool d_isAssume;
 };
 
 /** Declares a sygus invariant constraint

diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index 279761b43d8b8cd9325182483104dc77a9ae3f97..46e83e9e7a804248a74224dff9def8249854c290 100644 (file)
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -994,11 +994,11 @@ void SmtEngine::declareSynthFun(Node func,
   declareSynthFun(func, sygusType, isInv, vars);
 }
 
-void SmtEngine::assertSygusConstraint(Node constraint)
+void SmtEngine::assertSygusConstraint(Node n, bool isAssume)
 {
   SmtScope smts(this);
   finishInit();
-  d_sygusSolver->assertSygusConstraint(constraint);
+  d_sygusSolver->assertSygusConstraint(n, isAssume);
 }
 
 void SmtEngine::assertSygusInvConstraint(Node inv,

diff --git a/src/smt/smt_engine.h b/src/smt/smt_engine.h
index 06a1c9ae4785cca242a6e7981f0a9bd260415eeb..9f17fa27ebd5d93f9c6583f01c86c22045b89ff4 100644 (file)
--- a/src/smt/smt_engine.h
+++ b/src/smt/smt_engine.h
@@ -416,8 +416,12 @@ class CVC5_EXPORT SmtEngine
    */
   void declareSynthFun(Node func, bool isInv, const std::vector<Node>& vars);
 
-  /** Add a regular sygus constraint.*/
-  void assertSygusConstraint(Node constraint);
+  /**
+   * Add a regular sygus constraint or assumption.
+   * @param n The formula
+   * @param isAssume True if n is an assumption.
+   */
+  void assertSygusConstraint(Node n, bool isAssume = false);
 
   /**
    * Add an invariant constraint.

diff --git a/src/smt/sygus_solver.cpp b/src/smt/sygus_solver.cpp
index 32a0ee22033f82c5ffe8a421bb2b4fa482c07582..ff701ec48e7e3178eb8b489e670c09005bd63ec6 100644 (file)
--- a/src/smt/sygus_solver.cpp
+++ b/src/smt/sygus_solver.cpp
@@ -90,10 +90,18 @@ void SygusSolver::declareSynthFun(Node fn,
   setSygusConjectureStale();
 }
 
-void SygusSolver::assertSygusConstraint(Node constraint)
+void SygusSolver::assertSygusConstraint(Node n, bool isAssume)
 {
-  Trace("smt") << "SygusSolver::assertSygusConstrant: " << constraint << "\n";
-  d_sygusConstraints.push_back(constraint);
+  Trace("smt") << "SygusSolver::assertSygusConstrant: " << n
+               << ", isAssume=" << isAssume << "\n";
+  if (isAssume)
+  {
+    d_sygusAssumps.push_back(n);
+  }
+  else
+  {
+    d_sygusConstraints.push_back(n);
+  }
 
   // sygus conjecture is now stale
   setSygusConjectureStale();
@@ -186,13 +194,14 @@ Result SygusSolver::checkSynth(Assertions& as)
     NodeManager* nm = NodeManager::currentNM();
     // build synthesis conjecture from asserted constraints and declared
     // variables/functions
-    std::vector<Node> bodyv;
     Trace("smt") << "Sygus : Constructing sygus constraint...\n";
-    size_t nconstraints = d_sygusConstraints.size();
-    Node body = nconstraints == 0
-                    ? nm->mkConst(true)
-                    : (nconstraints == 1 ? d_sygusConstraints[0]
-                                         : nm->mkNode(AND, d_sygusConstraints));
+    Node body = nm->mkAnd(d_sygusConstraints);
+    // note that if there are no constraints, then assumptions are irrelevant
+    if (!d_sygusConstraints.empty() && !d_sygusAssumps.empty())
+    {
+      Node bodyAssump = nm->mkAnd(d_sygusAssumps);
+      body = nm->mkNode(IMPLIES, bodyAssump, body);
+    }
     body = body.notNode();
     Trace("smt") << "...constructed sygus constraint " << body << std::endl;
     if (!d_sygusVars.empty())

diff --git a/src/smt/sygus_solver.h b/src/smt/sygus_solver.h
index 3db61503762c4bf5b2d68d51a872e3cdc24c128c..90a6a87f02da4abf88f22eff1262b425fe746874 100644 (file)
--- a/src/smt/sygus_solver.h
+++ b/src/smt/sygus_solver.h
@@ -82,8 +82,8 @@ class SygusSolver
                        bool isInv,
                        const std::vector<Node>& vars);
 
-  /** Add a regular sygus constraint.*/
-  void assertSygusConstraint(Node constraint);
+  /** Add a regular sygus constraint or assumption.*/
+  void assertSygusConstraint(Node n, bool isAssume);
 
   /**
    * Add an invariant constraint.
@@ -185,6 +185,8 @@ class SygusSolver
   std::vector<Node> d_sygusVars;
   /** sygus constraints */
   std::vector<Node> d_sygusConstraints;
+  /** sygus assumptions */
+  std::vector<Node> d_sygusAssumps;
   /** functions-to-synthesize */
   std::vector<Node> d_sygusFunSymbols;
   /**

diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index fd734b321fe4282f30e9b759a0a8168b2c6fb956..90ad99e70a81a26e0b33ac84939a46e57fc91f5d 100644 (file)
--- a/test/regress/CMakeLists.txt
+++ b/test/regress/CMakeLists.txt
@@ -1241,6 +1241,7 @@ set(regress_0_tests
   regress0/strings/unicode-esc.smt2
   regress0/strings/unsound-0908.smt2
   regress0/strings/unsound-repl-rewrite.smt2
+  regress0/sygus/assume-simple.sy
   regress0/sygus/array-grammar-select.sy
   regress0/sygus/ccp16.lus.sy
   regress0/sygus/cegqi-si-string-triv-2fun.sy
@@ -2398,6 +2399,7 @@ set(regress_1_tests
   regress1/sygus/re-concat.sy
   regress1/sygus/repair-const-rl.sy
   regress1/sygus/replicate-mod.sy
+  regress1/sygus/replicate-mod-assume.sy
   regress1/sygus/rex-strings-alarm.sy
   regress1/sygus/sets-pred-test.sy
   regress1/sygus/simple-regexp.sy

diff --git a/test/regress/regress0/sygus/assume-simple.sy b/test/regress/regress0/sygus/assume-simple.sy
new file mode 100644 (file)
index 0000000..58f3753
--- /dev/null
+++ b/test/regress/regress0/sygus/assume-simple.sy
@@ -0,0 +1,13 @@
+; EXPECT: unsat
+; COMMAND-LINE: --sygus-out=status
+
+(set-logic LIA)
+(synth-fun f ((x Int)) Int
+  ((Start Int))
+  ((Start Int (x 0 1 (+ Start Start)))))
+(declare-var y Int)
+(assume (>= y 0))
+(constraint (>= (f y) 0))
+(constraint (>= (f y) y))
+; lambda x. x is a valid solution
+(check-synth)

diff --git a/test/regress/regress0/sygus/pLTL-sygus-syntax-err.sy b/test/regress/regress0/sygus/pLTL-sygus-syntax-err.sy
index 6a149cc7111af0b84c477df66cbc311a7ebbc17f..cf8e4da31656bd9238644bf41fc91c971cb25113 100644 (file)
--- a/test/regress/regress0/sygus/pLTL-sygus-syntax-err.sy
+++ b/test/regress/regress0/sygus/pLTL-sygus-syntax-err.sy
@@ -1,6 +1,6 @@
 ; REQUIRES: no-competition
 ; COMMAND-LINE: --sygus-out=status --sygus-rec-fun --lang=sygus2
-; EXPECT-ERROR: (error "Parse Error: pLTL-sygus-syntax-err.sy:80.19: number of arguments does not match the constructor type
+; EXPECT-ERROR: (error "Parse Error: pLTL-sygus-syntax-err.sy:78.19: number of arguments does not match the constructor type
 ; EXPECT-ERROR:
 ; EXPECT-ERROR: (Op2 <O2> <F>)
 ; EXPECT-ERROR: ^
@@ -31,8 +31,6 @@
 )
 
 ; Trace Length.
-(declare-const tn Int)
-(assert (= tn 2))
 
 ;cTrace Declaration (trace_index, variable_index)
 (define-fun val ((i Int) (x Var)) Bool
@@ -44,7 +42,7 @@
 
 ;cpLTL Semantics
 (define-fun-rec holds ((f Formula) (t Time)) Bool
-  (and (<= 0 t tn)
+  (and (<= 0 t 2)
        (match f (
          ((P i) (val t i))
 
@@ -54,7 +52,7 @@
 
              (Y (and (< 0 t) (holds g (- t 1))))
 
-             (G (and (holds g t) (or (= t tn) (holds f (+ t 1)))))
+             (G (and (holds g t) (or (= t 2) (holds f (+ t 1)))))
 
              (H (and (holds g t) (or (= t 0) (holds f (- t 1)))))
           )))

diff --git a/test/regress/regress1/sygus/replicate-mod-assume.sy b/test/regress/regress1/sygus/replicate-mod-assume.sy
new file mode 100644 (file)
index 0000000..c10cab2
--- /dev/null
+++ b/test/regress/regress1/sygus/replicate-mod-assume.sy
@@ -0,0 +1,157 @@
+; EXPECT: unsat
+; COMMAND-LINE: --sygus-out=status
+(set-logic LIA)
+(synth-fun fr0 ((_v Int) (n Int) (x Int)) Int
+       )
+(synth-fun fr1 ((_v Int) (n Int) (x Int)) Int
+       )
+(synth-fun fr10 ((_v Int) (n Int) (x Int)) Int
+       )
+(synth-fun fr11 ((_v Int) (n Int) (x Int)) Int
+       )
+(synth-fun fr12 ((_v Int) (n Int) (x Int)) Int
+       )
+(synth-fun fr13 ((_v Int) (n Int) (x Int)) Int
+       )
+(synth-fun fr14 ((_v Int) (n Int) (x Int)) Int
+       )
+(synth-fun fr15 ((_v Int) (n Int) (x Int)) Int
+       )
+(synth-fun fr16 ((_v Int) (n Int) (x Int)) Int
+       )
+(synth-fun fr17 ((_v Int) (n Int) (x Int)) Int
+       )
+(synth-fun fr18 ((_v Int) (n Int) (x Int)) Int
+       )
+(synth-fun fr19 ((_v Int) (n Int) (x Int)) Int
+       )
+(synth-fun fr2 ((_v Int) (n Int) (x Int)) Int
+       )
+(synth-fun fr20 ((_v Int) (n Int) (x Int)) Int
+       )
+(synth-fun fr21 ((_v Int) (n Int) (x Int)) Int
+       )
+(synth-fun fr22 ((_v Int) (n Int) (x Int)) Int
+       )
+(synth-fun fr23 ((_v Int) (n Int) (x Int)) Int
+       )
+(synth-fun fr24 ((_v Int) (n Int) (x Int)) Int
+       )
+(synth-fun fr25 ((_v Int) (n Int) (x Int)) Int
+       )
+(synth-fun fr26 ((_v Int) (n Int) (x Int)) Int
+       )
+(synth-fun fr27 ((_v Int) (n Int) (x Int)) Int
+       )
+(synth-fun fr28 ((_v Int) (n Int) (x Int)) Int
+       )
+(synth-fun fr29 ((_v Int) (n Int) (x Int)) Int
+       )
+(synth-fun fr3 ((_v Int) (n Int) (x Int)) Int
+       )
+(synth-fun fr30 ((_v Int) (n Int) (x Int)) Int
+       )
+(synth-fun fr31 ((_v Int) (n Int) (x Int)) Int
+       )
+(synth-fun fr32 ((_v Int) (n Int) (x Int)) Int
+       )
+(synth-fun fr33 ((_v Int) (n Int) (x Int)) Int
+       )
+(synth-fun fr34 ((_v Int) (n Int) (x Int)) Int
+       )
+(synth-fun fr35 ((_v Int) (n Int) (x Int)) Int
+       )
+(synth-fun fr36 ((_v Int) (n Int) (x Int)) Int
+       )
+(synth-fun fr4 ((_v Int) (n Int) (x Int)) Int
+       )
+(synth-fun fr5 ((_v Int) (n Int) (x Int)) Int
+       )
+(synth-fun fr6 ((_v Int) (n Int) (x Int)) Int
+       )
+(synth-fun fr7 ((_v Int) (n Int) (x Int)) Int
+       )
+(synth-fun fr8 ((_v Int) (n Int) (x Int)) Int
+       )
+(synth-fun fr9 ((_v Int) (n Int) (x Int)) Int
+       )
+(synth-fun m0 ((_v Int) (n Int) (x Int)) Int
+       )
+(synth-fun m1 ((_v Int) (n Int) (x Int)) Int
+       )
+(synth-fun m10 ((_v Int) (n Int) (x Int)) Int
+       )
+(synth-fun m11 ((_v Int) (n Int) (x Int)) Int
+       )
+(synth-fun m12 ((_v Int) (n Int) (x Int)) Int
+       )
+(synth-fun m13 ((_v Int) (n Int) (x Int)) Int
+       )
+(synth-fun m14 ((_v Int) (n Int) (x Int)) Int
+       )
+(synth-fun m15 ((_v Int) (n Int) (x Int)) Int
+       )
+(synth-fun m16 ((_v Int) (n Int) (x Int)) Int
+       )
+(synth-fun m17 ((_v Int) (n Int) (x Int)) Int
+       )
+(synth-fun m2 ((_v Int) (n Int) (x Int)) Int
+       )
+(synth-fun m3 ((_v Int) (n Int) (x Int)) Int
+       )
+(synth-fun m4 ((_v Int) (n Int) (x Int)) Int
+       )
+(synth-fun m5 ((_v Int) (n Int) (x Int)) Int
+       )
+(synth-fun m6 ((_v Int) (n Int) (x Int)) Int
+       )
+(synth-fun m7 ((_v Int) (n Int) (x Int)) Int
+       )
+(synth-fun m8 ((_v Int) (n Int) (x Int)) Int
+       )
+(synth-fun m9 ((_v Int) (n Int) (x Int)) Int
+       )
+(synth-fun p0 ((_v Int) (n Int) (x Int)) Int)
+(synth-fun p1 ((_v Int) (n Int) (x Int)) Int)
+(synth-fun p2 ((_v Int) (n Int) (x Int)) Int)
+(synth-fun p3 ((_v Int) (n Int) (x Int)) Int)
+(synth-fun p4 ((_v Int) (n Int) (x Int)) Int)
+(synth-fun p5 ((_v Int) (n Int) (x Int)) Int)
+(declare-var n Int)
+(declare-var x Int)
+(declare-var x10 Int)
+(declare-var x11 Int)
+(declare-var x14 Int)
+(declare-var x15 Int)
+(declare-var x2 Int)
+(declare-var x3 Int)
+(declare-var x6 Int)
+(declare-var x7 Int)
+(declare-var _v Int)
+(assume (and (= false (<= n 0)) (>= n 0)))
+(constraint (>= (p4 _v n x) 0))
+(constraint (and (and (and (>= (m6 _v n x) 0) (>= (m8 _v n x) 0)) (>= (m9 _v n x) 0)) (= (m6 _v n x) (+ (m8 _v n x) (m9 _v n x)))))
+(constraint (and (and (and (>= (fr17 _v n x) 0) (>= (fr19 _v n x) 0)) (>= (fr20 _v n x) 0)) (= (fr17 _v n x) (+ (fr19 _v n x) (fr20 _v n x)))))
+(constraint (and (and (and (>= (fr15 _v n x) 0) (>= (fr17 _v n x) 0)) (>= (fr18 _v n x) 0)) (= (fr15 _v n x) (+ (fr17 _v n x) (fr18 _v n x)))))
+(constraint (and (and (and (>= (m1 _v n x) 0) (>= (m6 _v n x) 0)) (>= (m7 _v n x) 0)) (= (m1 _v n x) (+ (m6 _v n x) (m7 _v n x)))))
+(constraint (and (and (and (>= (fr13 _v n x) 0) (>= (fr15 _v n x) 0)) (>= (fr16 _v n x) 0)) (= (fr13 _v n x) (+ (fr15 _v n x) (fr16 _v n x)))))
+(constraint (and (and (and (>= (fr12 _v n x) 0) (>= (fr13 _v n x) 0)) (>= (fr14 _v n x) 0)) (= (fr12 _v n x) (+ (fr13 _v n x) (fr14 _v n x)))))
+(constraint (and (and (and (and (and (and (= (+ (+ (+ 0 (p1 _v n x)) (fr1 _v n x)) 0) (+ (+ (+ 0 0) (fr12 _v n x)) 0)) (>= (fr1 _v n x) 0)) (>= (fr12 _v n x) 0)) (>= 0 0)) (>= 0 0)) (>= 0 0)) (>= 0 0)))
+(constraint (=> (and (and (= false (<= n 0)) (= _v x)) (>= n 0)) (>= 0 (+ (p4 _v n x) (- (+ (fr18 _v n x) 0))))))
+(constraint (>= 0 (- (+ (fr14 _v n x) 0))))
+(constraint (>= (p5 _v n x) (p4 _v n x)))
+(constraint (>= (p5 _v n x) 0))
+(constraint (and (and (and (>= (m10 _v n x) 0) (>= (m12 _v n x) 0)) (>= (m13 _v n x) 0)) (= (m10 _v n x) (+ (m12 _v n x) (m13 _v n x)))))
+(constraint (and (and (and (>= (fr25 _v n x) 0) (>= (fr27 _v n x) 0)) (>= (fr28 _v n x) 0)) (= (fr25 _v n x) (+ (fr27 _v n x) (fr28 _v n x)))))
+(constraint (and (and (and (>= (fr23 _v n x) 0) (>= (fr25 _v n x) 0)) (>= (fr26 _v n x) 0)) (= (fr23 _v n x) (+ (fr25 _v n x) (fr26 _v n x)))))
+(constraint (and (and (and (>= (m7 _v n x) 0) (>= (m10 _v n x) 0)) (>= (m11 _v n x) 0)) (= (m7 _v n x) (+ (m10 _v n x) (m11 _v n x)))))
+(constraint (and (and (and (>= (fr21 _v n x) 0) (>= (fr23 _v n x) 0)) (>= (fr24 _v n x) 0)) (= (fr21 _v n x) (+ (fr23 _v n x) (fr24 _v n x)))))
+(constraint (and (and (and (>= (- (fr16 _v n x) 1) 0) (>= (fr21 _v n x) 0)) (>= (fr22 _v n x) 0)) (= (- (fr16 _v n x) 1) (+ (fr21 _v n x) (fr22 _v n x)))))
+(constraint (=> false (>= 0 (- (+ (fr26 _v n x) 0)))))
+(constraint (and (and (and (>= (m14 _v n x) 0) (>= (m16 _v n x) 0)) (>= (m17 _v n x) 0)) (= (m14 _v n x) (+ (m16 _v n x) (m17 _v n x)))))
+(constraint (and (and (and (>= (fr33 _v n x) 0) (>= (fr35 _v n x) 0)) (>= (fr36 _v n x) 0)) (= (fr33 _v n x) (+ (fr35 _v n x) (fr36 _v n x)))))
+(constraint (and (and (and (>= (fr31 _v n x) 0) (>= (fr33 _v n x) 0)) (>= (fr34 _v n x) 0)) (= (fr31 _v n x) (+ (fr33 _v n x) (fr34 _v n x)))))
+(constraint (and (and (and (>= (m13 _v n x) 0) (>= (m14 _v n x) 0)) (>= (m15 _v n x) 0)) (= (m13 _v n x) (+ (m14 _v n x) (m15 _v n x)))))
+(constraint (and (and (and (>= (fr29 _v n x) 0) (>= (fr31 _v n x) 0)) (>= (fr32 _v n x) 0)) (= (fr29 _v n x) (+ (fr31 _v n x) (fr32 _v n x)))))
+(constraint (and (and (and (>= (fr28 _v n x) 0) (>= (fr29 _v n x) 0)) (>= (fr30 _v n x) 0)) (= (fr28 _v n x) (+ (fr29 _v n x) (fr30 _v n x)))))
+(check-synth)

diff --git a/test/unit/api/solver_black.cpp b/test/unit/api/solver_black.cpp
index 1f6f7801e5ec330ea9adc488916eb83fcc943c20..9042209e28765fec92ace729b16c760bdf1f4b2a 100644 (file)
--- a/test/unit/api/solver_black.cpp
+++ b/test/unit/api/solver_black.cpp
@@ -2300,6 +2300,20 @@ TEST_F(TestApiBlackSolver, addSygusConstraint)
   ASSERT_THROW(slv.addSygusConstraint(boolTerm), CVC5ApiException);
 }
 
+TEST_F(TestApiBlackSolver, addSygusAssume)
+{
+  Term nullTerm;
+  Term boolTerm = d_solver.mkBoolean(false);
+  Term intTerm = d_solver.mkInteger(1);
+
+  ASSERT_NO_THROW(d_solver.addSygusAssume(boolTerm));
+  ASSERT_THROW(d_solver.addSygusAssume(nullTerm), CVC5ApiException);
+  ASSERT_THROW(d_solver.addSygusAssume(intTerm), CVC5ApiException);
+
+  Solver slv;
+  ASSERT_THROW(slv.addSygusAssume(boolTerm), CVC5ApiException);
+}
+
 TEST_F(TestApiBlackSolver, addSygusInvConstraint)
 {
   Sort boolean = d_solver.getBooleanSort();