From 74c5067d81b8384701cff7f6e7b697d7fe67cf58 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Tue, 14 Sep 2021 16:29:32 -0500 Subject: [PATCH] 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. --- src/api/cpp/cvc5.cpp | 16 +- src/api/cpp/cvc5.h | 10 ++ src/parser/smt2/Smt2.g | 14 +- src/printer/printer.cpp | 5 + src/printer/printer.h | 3 + src/printer/smt2/smt2_printer.cpp | 5 + src/printer/smt2/smt2_printer.h | 3 + src/smt/command.cpp | 27 ++- src/smt/command.h | 4 +- src/smt/smt_engine.cpp | 4 +- src/smt/smt_engine.h | 8 +- src/smt/sygus_solver.cpp | 27 ++- src/smt/sygus_solver.h | 6 +- test/regress/CMakeLists.txt | 2 + test/regress/regress0/sygus/assume-simple.sy | 13 ++ .../regress0/sygus/pLTL-sygus-syntax-err.sy | 8 +- .../regress1/sygus/replicate-mod-assume.sy | 157 ++++++++++++++++++ test/unit/api/solver_black.cpp | 14 ++ 18 files changed, 295 insertions(+), 31 deletions(-) create mode 100644 test/regress/regress0/sygus/assume-simple.sy create mode 100644 test/regress/regress1/sygus/replicate-mod-assume.sy diff --git a/src/api/cpp/cvc5.cpp b/src/api/cpp/cvc5.cpp index 1aa9a740f..03c464e08 100644 --- 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 9324e4209..684b89114 100644 --- 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 ) + * \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 22a042951..2c391169c 100644 --- a/src/parser/smt2/Smt2.g +++ b/src/parser/smt2/Smt2.g @@ -518,6 +518,7 @@ sygusCommand returns [std::unique_ptr cmd] std::vector > sortedVarNames; std::vector sygusVars; std::string name; + bool isAssume; bool isInv; cvc5::api::Grammar* grammar = nullptr; } @@ -568,14 +569,13 @@ sygusCommand returns [std::unique_ptr 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* 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 9bd68e697..01fa7a9fd 100644 --- 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 5ffe07f77..499a9398f 100644 --- 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 0d556c1dc..07c5b10d8 100644 --- 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 729caebf4..fd7e0c7ac 100644 --- 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 adfd2f71d..4b04abcb2 100644 --- 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 b374a48c9..7587aaa63 100644 --- 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 279761b43..46e83e9e7 100644 --- 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 06a1c9ae4..9f17fa27e 100644 --- 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& 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 32a0ee220..ff701ec48 100644 --- 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 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 3db615037..90a6a87f0 100644 --- a/src/smt/sygus_solver.h +++ b/src/smt/sygus_solver.h @@ -82,8 +82,8 @@ class SygusSolver bool isInv, const std::vector& 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 d_sygusVars; /** sygus constraints */ std::vector d_sygusConstraints; + /** sygus assumptions */ + std::vector d_sygusAssumps; /** functions-to-synthesize */ std::vector d_sygusFunSymbols; /** diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt index fd734b321..90ad99e70 100644 --- 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 index 000000000..58f3753d8 --- /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 6a149cc71..cf8e4da31 100644 --- 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 ) ; 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 index 000000000..c10cab2f5 --- /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 1f6f7801e..9042209e2 100644 --- 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(); -- 2.30.2