diff options
40 files changed, 1360 insertions, 897 deletions
diff --git a/INSTALL.md b/INSTALL.md index 98cef2061..dc0de6cb4 100644 --- a/INSTALL.md +++ b/INSTALL.md @@ -151,7 +151,8 @@ provided with CVC4. ### CxxTest Unit Testing Framework (Unit Tests) [CxxTest](http://cxxtest.com) is required to optionally run CVC4's unit tests -(included with the distribution). See [Testing](testing) below for more details. +(included with the distribution). +See [Testing CVC4](#Testing-CVC4) below for more details. ## Building CVC4 diff --git a/configure.sh b/configure.sh index 1cc104c94..d5f466ec6 100755 --- a/configure.sh +++ b/configure.sh @@ -53,7 +53,7 @@ The following flags enable optional packages (disable with --no-<option name>). --glpk use GLPK simplex solver --abc use the ABC AIG library --cadical use the CaDiCaL SAT solver - --cryptominisat use the CryptoMiniSat sat solver + --cryptominisat use the CryptoMiniSat SAT solver --lfsc use the LFSC proof checker --symfpu use SymFPU for floating point solver --portfolio build the multithreaded portfolio version of CVC4 @@ -197,8 +197,8 @@ do --debug-symbols) debug_symbols=ON;; --no-debug-symbols) debug_symbols=OFF;; - --debug-context-memory-manager) debug_context_mm=ON;; - --no-debug-context-memory-manager) debug_context_mm=OFF;; + --debug-context-mm) debug_context_mm=ON;; + --no-debug-context-mm) debug_context_mm=OFF;; --dumping) dumping=ON;; --no-dumping) dumping=OFF;; diff --git a/src/api/cvc4cpp.cpp b/src/api/cvc4cpp.cpp index be7c5c665..b4d3b013d 100644 --- a/src/api/cvc4cpp.cpp +++ b/src/api/cvc4cpp.cpp @@ -749,15 +749,6 @@ Sort::Sort(const CVC4::Type& t) : d_type(new CVC4::Type(t)) {} Sort::~Sort() {} -Sort& Sort::operator=(const Sort& s) -{ - if (this != &s) - { - *d_type = *s.d_type; - } - return *this; -} - bool Sort::operator==(const Sort& s) const { return *d_type == *s.d_type; } bool Sort::operator!=(const Sort& s) const { return *d_type != *s.d_type; } @@ -1008,15 +999,6 @@ Term::Term(const CVC4::Expr& e) : d_expr(new CVC4::Expr(e)) {} Term::~Term() {} -Term& Term::operator=(const Term& t) -{ - if (this != &t) - { - *d_expr = *t.d_expr; - } - return *this; -} - bool Term::operator==(const Term& t) const { return *d_expr == *t.d_expr; } bool Term::operator!=(const Term& t) const { return *d_expr != *t.d_expr; } @@ -1180,15 +1162,6 @@ OpTerm::OpTerm(const CVC4::Expr& e) : d_expr(new CVC4::Expr(e)) {} OpTerm::~OpTerm() {} -OpTerm& OpTerm::operator=(const OpTerm& t) -{ - if (this != &t) - { - *d_expr = *t.d_expr; - } - return *this; -} - bool OpTerm::operator==(const OpTerm& t) const { return *d_expr == *t.d_expr; } bool OpTerm::operator!=(const OpTerm& t) const { return *d_expr != *t.d_expr; } diff --git a/src/api/cvc4cpp.h b/src/api/cvc4cpp.h index fc07a1cd7..aebeffb0d 100644 --- a/src/api/cvc4cpp.h +++ b/src/api/cvc4cpp.h @@ -197,13 +197,6 @@ class CVC4_PUBLIC Sort ~Sort(); /** - * Assignment operator. - * @param s the sort to assign to this sort - * @return this sort after assignment - */ - Sort& operator=(const Sort& s); - - /** * Comparison for structural equality. * @param s the sort to compare to * @return true if the sorts are equal @@ -554,14 +547,6 @@ class CVC4_PUBLIC Term ~Term(); /** - * Assignment operator, makes a copy of the given term. - * Both terms must belong to the same solver object. - * @param t the term to assign - * @return the reference to this term after assignment - */ - Term& operator=(const Term& t); - - /** * Syntactic equality operator. * Return true if both terms are syntactically identical. * Both terms must belong to the same solver object. @@ -844,14 +829,6 @@ class CVC4_PUBLIC OpTerm ~OpTerm(); /** - * Assignment operator, makes a copy of the given operator term. - * Both terms must belong to the same solver object. - * @param t the term to assign - * @return the reference to this operator term after assignment - */ - OpTerm& operator=(const OpTerm& t); - - /** * Syntactic equality operator. * Return true if both operator terms are syntactically identical. * Both operator terms must belong to the same solver object. diff --git a/src/options/options_handler.cpp b/src/options/options_handler.cpp index e4c0276ea..565f28334 100644 --- a/src/options/options_handler.cpp +++ b/src/options/options_handler.cpp @@ -538,6 +538,9 @@ enum \n\ var-agnostic \n\ + Use sygus solver to enumerate terms that are agnostic to variables. \n\ \n\ +auto (default) \n\ ++ Internally decide the best policy for each enumerator. \n\ +\n\ "; const std::string OptionsHandler::s_macrosQuantHelp = "\ @@ -987,6 +990,10 @@ OptionsHandler::stringToSygusActiveGenMode(std::string option, { return theory::quantifiers::SYGUS_ACTIVE_GEN_VAR_AGNOSTIC; } + else if (optarg == "auto") + { + return theory::quantifiers::SYGUS_ACTIVE_GEN_AUTO; + } else if (optarg == "help") { puts(s_sygusActiveGenHelp.c_str()); diff --git a/src/options/quantifiers_modes.h b/src/options/quantifiers_modes.h index 392393a91..05388cdf6 100644 --- a/src/options/quantifiers_modes.h +++ b/src/options/quantifiers_modes.h @@ -272,6 +272,8 @@ enum SygusActiveGenMode SYGUS_ACTIVE_GEN_ENUM, /** use variable-agnostic enumerators */ SYGUS_ACTIVE_GEN_VAR_AGNOSTIC, + /** internally decide the best policy for each enumerator */ + SYGUS_ACTIVE_GEN_AUTO, }; enum MacrosQuantMode { diff --git a/src/options/quantifiers_options.toml b/src/options/quantifiers_options.toml index 0b28c6a27..c555c37bf 100644 --- a/src/options/quantifiers_options.toml +++ b/src/options/quantifiers_options.toml @@ -1044,7 +1044,7 @@ header = "options/quantifiers_options.h" category = "regular" long = "sygus-active-gen=MODE" type = "CVC4::theory::quantifiers::SygusActiveGenMode" - default = "CVC4::theory::quantifiers::SYGUS_ACTIVE_GEN_NONE" + default = "CVC4::theory::quantifiers::SYGUS_ACTIVE_GEN_AUTO" handler = "stringToSygusActiveGenMode" includes = ["options/quantifiers_modes.h"] read_only = true @@ -1135,7 +1135,7 @@ header = "options/quantifiers_options.h" category = "regular" long = "sygus-pbe-multi-fair" type = "bool" - default = "true" + default = "false" help = "when using multiple enumerators, ensure that we only register value of minimial term size" [[option]] diff --git a/src/theory/datatypes/datatypes_sygus.cpp b/src/theory/datatypes/datatypes_sygus.cpp index a7763bff1..4c7dcec9a 100644 --- a/src/theory/datatypes/datatypes_sygus.cpp +++ b/src/theory/datatypes/datatypes_sygus.cpp @@ -1304,7 +1304,8 @@ void SygusSymBreakNew::preRegisterTerm( TNode n, std::vector< Node >& lemmas ) } } -void SygusSymBreakNew::registerSizeTerm( Node e, std::vector< Node >& lemmas ) { +void SygusSymBreakNew::registerSizeTerm(Node e, std::vector<Node>& lemmas) +{ if (d_register_st.find(e) != d_register_st.end()) { // already registered @@ -1545,15 +1546,32 @@ void SygusSymBreakNew::check( std::vector< Node >& lemmas ) { { // symmetry breaking lemmas should only be for enumerators Assert(d_register_st[a]); - std::vector<Node> sbl; - d_tds->getSymBreakLemmas(a, sbl); - for (const Node& lem : sbl) + // If this is a non-basic enumerator, process its symmetry breaking + // clauses. Since this class is not responsible for basic enumerators, + // their symmetry breaking clauses are ignored. + if (!d_tds->isBasicEnumerator(a)) { - TypeNode tn = d_tds->getTypeForSymBreakLemma(lem); - unsigned sz = d_tds->getSizeForSymBreakLemma(lem); - registerSymBreakLemma(tn, lem, sz, a, lemmas); + std::vector<Node> sbl; + d_tds->getSymBreakLemmas(a, sbl); + for (const Node& lem : sbl) + { + if (d_tds->isSymBreakLemmaTemplate(lem)) + { + // register the lemma template + TypeNode tn = d_tds->getTypeForSymBreakLemma(lem); + unsigned sz = d_tds->getSizeForSymBreakLemma(lem); + registerSymBreakLemma(tn, lem, sz, a, lemmas); + } + else + { + Trace("dt-sygus-debug") + << "DT sym break lemma : " << lem << std::endl; + // it is a normal lemma + lemmas.push_back(lem); + } + } + d_tds->clearSymBreakLemmas(a); } - d_tds->clearSymBreakLemmas(a); } } if (!lemmas.empty()) @@ -1563,9 +1581,20 @@ void SygusSymBreakNew::check( std::vector< Node >& lemmas ) { } // register search values, add symmetry breaking lemmas if applicable - for( std::map< Node, bool >::iterator it = d_register_st.begin(); it != d_register_st.end(); ++it ){ - if( it->second ){ - Node prog = it->first; + std::vector<Node> es; + d_tds->getEnumerators(es); + bool needsRecheck = false; + // for each enumerator registered to d_tds + for (Node& prog : es) + { + if (d_register_st.find(prog) == d_register_st.end()) + { + // not yet registered, do so now + registerSizeTerm(prog, lemmas); + needsRecheck = true; + } + else + { Trace("dt-sygus-debug") << "Checking model value of " << prog << "..." << std::endl; Assert(prog.getType().isDatatype()); @@ -1624,14 +1653,12 @@ void SygusSymBreakNew::check( std::vector< Node >& lemmas ) { prog.setAttribute(ssbo, !isExc); } } - //register any measured terms that we haven't encountered yet (should only be invoked on first call to check - Trace("sygus-sb") << "Register size terms..." << std::endl; - std::vector< Node > mts; - d_tds->getEnumerators(mts); - for( unsigned i=0; i<mts.size(); i++ ){ - registerSizeTerm( mts[i], lemmas ); + Trace("sygus-sb") << "SygusSymBreakNew::check: finished." << std::endl; + if (needsRecheck) + { + Trace("sygus-sb") << " SygusSymBreakNew::rechecking..." << std::endl; + return check(lemmas); } - Trace("sygus-sb") << " SygusSymBreakNew::check: finished." << std::endl; if (Trace.isOn("cegqi-engine") && !d_szinfo.empty()) { diff --git a/src/theory/quantifiers/sygus/cegis.cpp b/src/theory/quantifiers/sygus/cegis.cpp index 79bec60ee..6aca71ca3 100644 --- a/src/theory/quantifiers/sygus/cegis.cpp +++ b/src/theory/quantifiers/sygus/cegis.cpp @@ -69,17 +69,10 @@ bool Cegis::processInitialize(Node n, { Trace("cegis") << "Initialize cegis..." << std::endl; unsigned csize = candidates.size(); - // We only can use actively-generated enumerators if there is only one - // function-to-synthesize. Otherwise, we would have to generate a "product" of - // two actively-generated enumerators. That is, given a conjecture with two - // functions-to-synthesize with enumerators e_f and e_g, if: - // e_f -> t1, ..., tn - // e_g -> s1, ..., sm - // This module would expect constructCandidates calls (e_f,e_g) -> (ti, sj) - // for each i,j. We do not do this and revert to the default behavior of - // this module instead. - bool isActiveGen = - options::sygusActiveGenMode() != SYGUS_ACTIVE_GEN_NONE && csize == 1; + // The role of enumerators is to be either the single solution or part of + // a solution involving multiple enumerators. + EnumeratorRole erole = + csize == 1 ? ROLE_ENUM_SINGLE_SOLUTION : ROLE_ENUM_MULTI_SOLUTION; // initialize an enumerator for each candidate for (unsigned i = 0; i < csize; i++) { @@ -98,13 +91,8 @@ bool Cegis::processInitialize(Node n, } } Trace("cegis") << std::endl; - // variable agnostic enumerators require an active guard - d_tds->registerEnumerator(candidates[i], - candidates[i], - d_parent, - isActiveGen, - do_repair_const, - isActiveGen); + d_tds->registerEnumerator( + candidates[i], candidates[i], d_parent, erole, do_repair_const); } return true; } diff --git a/src/theory/quantifiers/sygus/cegis_unif.cpp b/src/theory/quantifiers/sygus/cegis_unif.cpp index dbde79aae..18e313bf0 100644 --- a/src/theory/quantifiers/sygus/cegis_unif.cpp +++ b/src/theory/quantifiers/sygus/cegis_unif.cpp @@ -44,7 +44,12 @@ bool CegisUnif::processInitialize(Node n, std::map<Node, Node> pt_to_cond; // strategy lemmas for each strategy point std::map<Node, std::vector<Node>> strategy_lemmas; - // Initialize strategies for all functions-to-synhesize + // Initialize strategies for all functions-to-synthesize + // The role of non-unification enumerators is to be either the single solution + // or part of a solution involving multiple enumerators. + EnumeratorRole eroleNonUnif = candidates.size() == 1 + ? ROLE_ENUM_SINGLE_SOLUTION + : ROLE_ENUM_MULTI_SOLUTION; for (const Node& f : candidates) { // Init UNIF util for this candidate @@ -53,7 +58,7 @@ bool CegisUnif::processInitialize(Node n, if (!d_sygus_unif.usingUnif(f)) { Trace("cegis-unif") << "* non-unification candidate : " << f << std::endl; - d_tds->registerEnumerator(f, f, d_parent); + d_tds->registerEnumerator(f, f, d_parent, eroleNonUnif); d_non_unif_candidates.push_back(f); } else @@ -462,7 +467,8 @@ Node CegisUnifEnumDecisionStrategy::mkLiteral(unsigned n) exclude_cons, term_irrelevant); d_virtual_enum = nm->mkSkolem("_ve", vtn); - d_tds->registerEnumerator(d_virtual_enum, Node::null(), d_parent); + d_tds->registerEnumerator( + d_virtual_enum, Node::null(), d_parent, ROLE_ENUM_CONSTRAINED); } // if new_size is a power of two, then isPow2 returns log2(new_size)+1 // otherwise, this returns 0. In the case it returns 0, we don't care @@ -606,20 +612,17 @@ void CegisUnifEnumDecisionStrategy::setUpEnumerator(Node e, } // register the enumerator si.d_enums[index].push_back(e); - bool mkActiveGuard = false; - bool isActiveGen = false; + EnumeratorRole erole = ROLE_ENUM_CONSTRAINED; // if we are using a single independent enumerator for conditions, then we // allocate an active guard, and are eligible to use variable-agnostic // enumeration. if (options::sygusUnifCondIndependent() && index == 1) { - mkActiveGuard = true; - isActiveGen = options::sygusActiveGenMode() != SYGUS_ACTIVE_GEN_NONE; + erole = ROLE_ENUM_POOL; } Trace("cegis-unif-enum") << "* Registering new enumerator " << e << " to strategy point " << si.d_pt << "\n"; - d_tds->registerEnumerator( - e, si.d_pt, d_parent, mkActiveGuard, false, isActiveGen); + d_tds->registerEnumerator(e, si.d_pt, d_parent, erole, false); } void CegisUnifEnumDecisionStrategy::registerEvalPts( diff --git a/src/theory/quantifiers/sygus/enum_stream_substitution.cpp b/src/theory/quantifiers/sygus/enum_stream_substitution.cpp index 24770ade0..e8daa4256 100644 --- a/src/theory/quantifiers/sygus/enum_stream_substitution.cpp +++ b/src/theory/quantifiers/sygus/enum_stream_substitution.cpp @@ -608,8 +608,17 @@ bool EnumStreamSubstitution::CombinationState::getNextCombination() } void EnumStreamConcrete::initialize(Node e) { d_ess.initialize(e.getType()); } -void EnumStreamConcrete::addValue(Node v) { d_ess.resetValue(v); } -Node EnumStreamConcrete::getNext() { return d_ess.getNext(); } +void EnumStreamConcrete::addValue(Node v) +{ + d_ess.resetValue(v); + d_currTerm = d_ess.getNext(); +} +bool EnumStreamConcrete::increment() +{ + d_currTerm = d_ess.getNext(); + return !d_currTerm.isNull(); +} +Node EnumStreamConcrete::getCurrent() { return d_currTerm; } } // namespace quantifiers } // namespace theory } // namespace CVC4 diff --git a/src/theory/quantifiers/sygus/enum_stream_substitution.h b/src/theory/quantifiers/sygus/enum_stream_substitution.h index 38fa0627b..476a364ea 100644 --- a/src/theory/quantifiers/sygus/enum_stream_substitution.h +++ b/src/theory/quantifiers/sygus/enum_stream_substitution.h @@ -286,12 +286,16 @@ class EnumStreamConcrete : public EnumValGenerator void initialize(Node e) override; /** get that value v was enumerated */ void addValue(Node v) override; - /** get the next value enumerated by this class */ - Node getNext() override; + /** increment */ + bool increment() override; + /** get the current value enumerated by this class */ + Node getCurrent() override; private: /** stream substitution utility */ EnumStreamSubstitution d_ess; + /** the current term generated by this class */ + Node d_currTerm; }; } // namespace quantifiers diff --git a/src/theory/quantifiers/sygus/sygus_enumerator.cpp b/src/theory/quantifiers/sygus/sygus_enumerator.cpp index 61ab9007a..5c3e44a33 100644 --- a/src/theory/quantifiers/sygus/sygus_enumerator.cpp +++ b/src/theory/quantifiers/sygus/sygus_enumerator.cpp @@ -25,21 +25,78 @@ namespace theory { namespace quantifiers { SygusEnumerator::SygusEnumerator(TermDbSygus* tds, SynthConjecture* p) - : d_tds(tds), - d_parent(p), - d_tlEnum(nullptr), - d_abortSize(-1), - d_firstTime(false) + : d_tds(tds), d_parent(p), d_tlEnum(nullptr), d_abortSize(-1) { } void SygusEnumerator::initialize(Node e) { + Trace("sygus-enum") << "SygusEnumerator::initialize " << e << std::endl; d_enum = e; d_etype = d_enum.getType(); + Assert(d_etype.isDatatype()); + Assert(d_etype.getDatatype().isSygus()); d_tlEnum = getMasterEnumForType(d_etype); d_abortSize = options::sygusAbortSize(); - d_firstTime = true; + + // Get the statically registered symmetry breaking clauses for e, see if they + // can be used for speeding up the enumeration. + NodeManager* nm = NodeManager::currentNM(); + std::vector<Node> sbl; + d_tds->getSymBreakLemmas(e, sbl); + Node ag = d_tds->getActiveGuardForEnumerator(e); + Node truen = nm->mkConst(true); + // use TNode for substitute below + TNode agt = ag; + TNode truent = truen; + Assert(d_tcache.find(d_etype) != d_tcache.end()); + const Datatype& dt = d_etype.getDatatype(); + for (const Node& lem : sbl) + { + if (!d_tds->isSymBreakLemmaTemplate(lem)) + { + // substitute its active guard by true and rewrite + Node slem = lem.substitute(agt, truent); + slem = Rewriter::rewrite(slem); + // break into conjuncts + std::vector<Node> sblc; + if (slem.getKind() == AND) + { + for (const Node& slemc : slem) + { + sblc.push_back(slemc); + } + } + else + { + sblc.push_back(slem); + } + for (const Node& sbl : sblc) + { + Trace("sygus-enum") + << " symmetry breaking lemma : " << sbl << std::endl; + // if its a negation of a unit top-level tester, then this specifies + // that we should not enumerate terms whose top symbol is that + // constructor + if (sbl.getKind() == NOT) + { + Node a; + int tst = datatypes::DatatypesRewriter::isTester(sbl[0], a); + if (tst >= 0) + { + if (a == e) + { + Node cons = Node::fromExpr(dt[tst].getConstructor()); + Trace("sygus-enum") << " ...unit exclude constructor #" << tst + << ", constructor " << cons << std::endl; + d_sbExcTlCons.insert(cons); + } + } + } + // other symmetry breaking lemmas such as disjunctions are not used + } + } + } } void SygusEnumerator::addValue(Node v) @@ -47,17 +104,9 @@ void SygusEnumerator::addValue(Node v) // do nothing } -Node SygusEnumerator::getNext() +bool SygusEnumerator::increment() { return d_tlEnum->increment(); } +Node SygusEnumerator::getCurrent() { - if (d_firstTime) - { - d_firstTime = false; - } - else if (!d_tlEnum->increment()) - { - // no more values - return Node::null(); - } if (d_abortSize >= 0) { int cs = static_cast<int>(d_tlEnum->getCurrentSize()); @@ -70,14 +119,30 @@ Node SygusEnumerator::getNext() } } Node ret = d_tlEnum->getCurrent(); - Trace("sygus-enum") << "Enumerate : " << d_tds->sygusToBuiltin(ret) - << std::endl; + if (!ret.isNull() && !d_sbExcTlCons.empty()) + { + Assert(ret.hasOperator()); + // might be excluded by an externally provided symmetry breaking clause + if (d_sbExcTlCons.find(ret.getOperator()) != d_sbExcTlCons.end()) + { + Trace("sygus-enum-exc") + << "Exclude (external) : " << d_tds->sygusToBuiltin(ret) << std::endl; + ret = Node::null(); + } + } + if (Trace.isOn("sygus-enum")) + { + Trace("sygus-enum") << "Enumerate : "; + TermDbSygus::toStreamSygus("sygus-enum", ret); + Trace("sygus-enum") << std::endl; + } return ret; } SygusEnumerator::TermCache::TermCache() : d_tds(nullptr), d_pbe(nullptr), + d_isSygusType(false), d_numConClasses(0), d_sizeEnum(0), d_isComplete(false) @@ -241,33 +306,37 @@ bool SygusEnumerator::TermCache::addTerm(Node n) d_terms.push_back(n); return true; } - Node bn = d_tds->sygusToBuiltin(n); - Node bnr = d_tds->getExtRewriter()->extendedRewrite(bn); - // must be unique up to rewriting - if (d_bterms.find(bnr) != d_bterms.end()) - { - Trace("sygus-enum-exc") << "Exclude: " << bn << std::endl; - return false; - } - // if we are doing PBE symmetry breaking - if (d_pbe != nullptr) + Assert(!n.isNull()); + if (options::sygusSymBreakDynamic()) { - // Is it equivalent under examples? - Node bne = d_pbe->addSearchVal(d_tn, d_enum, bnr); - if (!bne.isNull()) + Node bn = d_tds->sygusToBuiltin(n); + Node bnr = d_tds->getExtRewriter()->extendedRewrite(bn); + // must be unique up to rewriting + if (d_bterms.find(bnr) != d_bterms.end()) { - if (bnr != bne) + Trace("sygus-enum-exc") << "Exclude: " << bn << std::endl; + return false; + } + // if we are doing PBE symmetry breaking + if (d_pbe != nullptr) + { + // Is it equivalent under examples? + Node bne = d_pbe->addSearchVal(d_tn, d_enum, bnr); + if (!bne.isNull()) { - Trace("sygus-enum-exc") << "Exclude (by examples): " << bn - << ", since we already have " << bne - << "!=" << bnr << std::endl; - return false; + if (bnr != bne) + { + Trace("sygus-enum-exc") << "Exclude (by examples): " << bn + << ", since we already have " << bne + << "!=" << bnr << std::endl; + return false; + } } } + Trace("sygus-enum-terms") << "tc(" << d_tn << "): term " << bn << std::endl; + d_bterms.insert(bnr); } - Trace("sygus-enum-terms") << "tc(" << d_tn << "): term " << bn << std::endl; d_terms.push_back(n); - d_bterms.insert(bnr); return true; } void SygusEnumerator::TermCache::pushEnumSizeIndex() @@ -302,7 +371,12 @@ void SygusEnumerator::TermCache::setComplete() { d_isComplete = true; } unsigned SygusEnumerator::TermEnum::getCurrentSize() { return d_currSize; } SygusEnumerator::TermEnum::TermEnum() : d_se(nullptr), d_currSize(0) {} SygusEnumerator::TermEnumSlave::TermEnumSlave() - : TermEnum(), d_sizeLim(0), d_index(0), d_indexNextEnd(0), d_master(nullptr) + : TermEnum(), + d_sizeLim(0), + d_index(0), + d_indexNextEnd(0), + d_hasIndexNextEnd(false), + d_master(nullptr) { } @@ -384,7 +458,7 @@ bool SygusEnumerator::TermEnumSlave::validateIndex() Trace("sygus-enum-debug2") << "slave(" << d_tn << ") : validate index...\n"; SygusEnumerator::TermCache& tc = d_se->d_tcache[d_tn]; // ensure that index is in the range - if (d_index >= tc.getNumTerms()) + while (d_index >= tc.getNumTerms()) { Assert(d_index == tc.getNumTerms()); Trace("sygus-enum-debug2") << "slave(" << d_tn << ") : force master...\n"; @@ -494,6 +568,7 @@ SygusEnumerator::TermEnum* SygusEnumerator::getMasterEnumForType(TypeNode tn) SygusEnumerator::TermEnumMaster::TermEnumMaster() : TermEnum(), d_isIncrementing(false), + d_currTermSet(false), d_consClassNum(0), d_ccWeight(0), d_consNum(0), @@ -515,6 +590,7 @@ bool SygusEnumerator::TermEnumMaster::initialize(SygusEnumerator* se, d_currChildSize = 0; d_ccCons.clear(); d_isIncrementing = false; + d_currTermSet = false; bool ret = increment(); Trace("sygus-enum-debug") << "master(" << tn << "): finish init, ret = " << ret << "\n"; @@ -523,10 +599,11 @@ bool SygusEnumerator::TermEnumMaster::initialize(SygusEnumerator* se, Node SygusEnumerator::TermEnumMaster::getCurrent() { - if (!d_currTerm.isNull()) + if (d_currTermSet) { return d_currTerm; } + d_currTermSet = true; // construct based on the children std::vector<Node> children; const Datatype& dt = d_tn.getDatatype(); @@ -538,7 +615,13 @@ Node SygusEnumerator::TermEnumMaster::getCurrent() for (unsigned i = 0, nargs = dt[cnum].getNumArgs(); i < nargs; i++) { Assert(d_children.find(i) != d_children.end()); - children.push_back(d_children[i].getCurrent()); + Node cc = d_children[i].getCurrent(); + if (cc.isNull()) + { + d_currTerm = cc; + return cc; + } + children.push_back(cc); } d_currTerm = NodeManager::currentNM()->mkNode(APPLY_CONSTRUCTOR, children); return d_currTerm; @@ -705,21 +788,27 @@ bool SygusEnumerator::TermEnumMaster::incrementInternal() Assert(d_childrenValid == d_ccTypes.size()); // do we have more constructors for the given children? - while (d_consNum < d_ccCons.size()) + if (d_consNum < d_ccCons.size()) { Trace("sygus-enum-debug2") << "master(" << d_tn << "): try constructor " << d_consNum << std::endl; // increment constructor index // we will build for the current constructor and the given children d_consNum++; + d_currTermSet = false; d_currTerm = Node::null(); Node c = getCurrent(); - if (tc.addTerm(c)) + if (!c.isNull()) { - return true; + if (!tc.addTerm(c)) + { + // the term was not unique based on rewriting + Trace("sygus-enum-debug2") << "master(" << d_tn + << "): failed addTerm\n"; + d_currTerm = Node::null(); + } } - Trace("sygus-enum-debug2") << "master(" << d_tn << "): failed addTerm\n"; - // the term was not unique based on rewriting + return true; } // finished constructors for this set of children, must increment children diff --git a/src/theory/quantifiers/sygus/sygus_enumerator.h b/src/theory/quantifiers/sygus/sygus_enumerator.h index 10a44da03..af6bb03f0 100644 --- a/src/theory/quantifiers/sygus/sygus_enumerator.h +++ b/src/theory/quantifiers/sygus/sygus_enumerator.h @@ -50,8 +50,10 @@ class SygusEnumerator : public EnumValGenerator void initialize(Node e) override; /** Inform this generator that abstract value v was enumerated. */ void addValue(Node v) override; + /** increment */ + bool increment() override; /** Get the next concrete value generated by this class. */ - Node getNext() override; + Node getCurrent() override; private: /** pointer to term database sygus */ @@ -322,6 +324,8 @@ class SygusEnumerator : public EnumValGenerator bool d_isIncrementing; /** cache for getCurrent() */ Node d_currTerm; + /** is d_currTerm set */ + bool d_currTermSet; //----------------------------- current constructor class information /** the next constructor class we are using */ unsigned d_consClassNum; @@ -429,10 +433,17 @@ class SygusEnumerator : public EnumValGenerator TermEnum* d_tlEnum; /** the abort size, caches the value of --sygus-abort-size */ int d_abortSize; - /** this flag is true for the first time to getNext() after initialize(e) */ - bool d_firstTime; /** get master enumerator for type tn */ TermEnum* getMasterEnumForType(TypeNode tn); + //-------------------------------- externally specified symmetry breaking + /** set of constructors we disallow at top level + * + * A constructor C is disallowed at the top level if a symmetry breaking + * lemma that entails ~is-C( d_enum ) was registered to + * TermDbSygus::registerSymBreakLemma. + */ + std::unordered_set<Node, NodeHashFunction> d_sbExcTlCons; + //-------------------------------- end externally specified symmetry breaking }; } // namespace quantifiers diff --git a/src/theory/quantifiers/sygus/sygus_grammar_cons.cpp b/src/theory/quantifiers/sygus/sygus_grammar_cons.cpp index 47c701cf6..d6dfb3d26 100644 --- a/src/theory/quantifiers/sygus/sygus_grammar_cons.cpp +++ b/src/theory/quantifiers/sygus/sygus_grammar_cons.cpp @@ -374,18 +374,24 @@ void CegGrammarConstructor::mkSygusConstantsForType(TypeNode type, // TODO #1178 : add other missing types } -void CegGrammarConstructor::collectSygusGrammarTypesFor( TypeNode range, std::vector< TypeNode >& types, std::map< TypeNode, std::vector< DatatypeConstructorArg > >& sels ){ +void CegGrammarConstructor::collectSygusGrammarTypesFor( + TypeNode range, std::vector<TypeNode>& types) +{ if( !range.isBoolean() ){ if( std::find( types.begin(), types.end(), range )==types.end() ){ Trace("sygus-grammar-def") << "...will make grammar for " << range << std::endl; types.push_back( range ); if( range.isDatatype() ){ - const Datatype& dt = ((DatatypeType)range.toType()).getDatatype(); - for( unsigned i=0; i<dt.getNumConstructors(); i++ ){ - for( unsigned j=0; j<dt[i].getNumArgs(); j++ ){ - TypeNode crange = TypeNode::fromType( ((SelectorType)dt[i][j].getType()).getRangeType() ); - sels[crange].push_back( dt[i][j] ); - collectSygusGrammarTypesFor( crange, types, sels ); + const Datatype& dt = range.getDatatype(); + for (unsigned i = 0, size = dt.getNumConstructors(); i < size; ++i) + { + for (unsigned j = 0, size_args = dt[i].getNumArgs(); j < size_args; + ++j) + { + collectSygusGrammarTypesFor( + TypeNode::fromType(static_cast<SelectorType>(dt[i][j].getType()) + .getRangeType()), + types); } } } @@ -408,76 +414,87 @@ void CegGrammarConstructor::mkSygusDefaultGrammar( << range << std::endl; // collect the variables std::vector<Node> sygus_vars; - if( !bvl.isNull() ){ - for( unsigned i=0; i<bvl.getNumChildren(); i++ ){ + if (!bvl.isNull()) + { + for (unsigned i = 0, size = bvl.getNumChildren(); i < size; ++i) + { if (term_irrelevant.find(bvl[i]) == term_irrelevant.end()) { sygus_vars.push_back(bvl[i]); } else { - Trace("sygus-grammar-def") << "...synth var " << bvl[i] - << " has been marked irrelevant." - << std::endl; + Trace("sygus-grammar-def") + << "...synth var " << bvl[i] << " has been marked irrelevant." + << std::endl; } } } - //if( !range.isBoolean() && !range.isInteger() && !range.isBitVector() && !range.isDatatype() ){ - // parseError("No default grammar for type."); - //} - std::vector< std::vector< Expr > > ops; + // operators for each constructor in type + std::vector<std::vector<Expr>> ops; + // names for the operators + std::vector<std::vector<std::string>> cnames; + // argument types of operators + std::vector<std::vector<std::vector<Type>>> cargs; + // set of callbacks for each constructor + std::vector<std::vector<std::shared_ptr<SygusPrintCallback>>> pcs; + // weights for each constructor + std::vector<std::vector<int>> weights; + // index of top datatype, i.e. the datatype for the range type int startIndex = -1; std::map< Type, Type > sygus_to_builtin; - std::vector< TypeNode > types; - std::map< TypeNode, std::vector< DatatypeConstructorArg > > sels; - //types for each of the variables of parametric sort - for( unsigned i=0; i<sygus_vars.size(); i++ ){ - collectSygusGrammarTypesFor( sygus_vars[i].getType(), types, sels ); + std::vector<TypeNode> types; + // collect connected types for each of the variables + for (unsigned i = 0, size = sygus_vars.size(); i < size; ++i) + { + collectSygusGrammarTypesFor(sygus_vars[i].getType(), types); } - //types connected to range - collectSygusGrammarTypesFor( range, types, sels ); + // collect connected types to range + collectSygusGrammarTypesFor(range, types); - //name of boolean sort + // create placeholder for boolean type (kept apart since not collected) std::stringstream ssb; ssb << fun << "_Bool"; std::string dbname = ssb.str(); Type unres_bt = mkUnresolvedType(ssb.str(), unres).toType(); + // create placeholders for collected types std::vector< Type > unres_types; std::map< TypeNode, Type > type_to_unres; - for( unsigned i=0; i<types.size(); i++ ){ + for (unsigned i = 0, size = types.size(); i < size; ++i) + { std::stringstream ss; ss << fun << "_" << types[i]; std::string dname = ss.str(); datatypes.push_back(Datatype(dname)); ops.push_back(std::vector< Expr >()); + cnames.push_back(std::vector<std::string>()); + cargs.push_back(std::vector<std::vector<Type>>()); + pcs.push_back(std::vector<std::shared_ptr<SygusPrintCallback>>()); + weights.push_back(std::vector<int>()); //make unresolved type Type unres_t = mkUnresolvedType(dname, unres).toType(); unres_types.push_back(unres_t); type_to_unres[types[i]] = unres_t; sygus_to_builtin[unres_t] = types[i].toType(); } - for( unsigned i=0; i<types.size(); i++ ){ + for (unsigned i = 0, size = types.size(); i < size; ++i) + { Trace("sygus-grammar-def") << "Make grammar for " << types[i] << " " << unres_types[i] << std::endl; - std::vector<std::string> cnames; - std::vector<std::vector<CVC4::Type> > cargs; - /* Print callbacks for each constructor */ - std::vector<std::shared_ptr<SygusPrintCallback>> pcs; - /* Weights for each constructor */ - std::vector<int> weights; Type unres_t = unres_types[i]; //add variables - for( unsigned j=0; j<sygus_vars.size(); j++ ){ + for (unsigned j = 0, size_j = sygus_vars.size(); j < size_j; ++j) + { if( sygus_vars[j].getType()==types[i] ){ std::stringstream ss; ss << sygus_vars[j]; Trace("sygus-grammar-def") << "...add for variable " << ss.str() << std::endl; ops[i].push_back( sygus_vars[j].toExpr() ); - cnames.push_back( ss.str() ); - cargs.push_back( std::vector< CVC4::Type >() ); - pcs.push_back(nullptr); - weights.push_back(-1); + cnames[i].push_back(ss.str()); + cargs[i].push_back(std::vector<Type>()); + pcs[i].push_back(nullptr); + weights[i].push_back(-1); } } //add constants @@ -486,33 +503,35 @@ void CegGrammarConstructor::mkSygusDefaultGrammar( std::map< TypeNode, std::vector< Node > >::iterator itec = extra_cons.find( types[i] ); if( itec!=extra_cons.end() ){ //consts.insert( consts.end(), itec->second.begin(), itec->second.end() ); - for( unsigned j=0; j<itec->second.size(); j++ ){ + for (unsigned j = 0, size_j = itec->second.size(); j < size_j; ++j) + { if( std::find( consts.begin(), consts.end(), itec->second[j] )==consts.end() ){ consts.push_back( itec->second[j] ); } } } - for( unsigned j=0; j<consts.size(); j++ ){ + for (unsigned j = 0, size_j = consts.size(); j < size_j; ++j) + { std::stringstream ss; ss << consts[j]; Trace("sygus-grammar-def") << "...add for constant " << ss.str() << std::endl; ops[i].push_back( consts[j].toExpr() ); - cnames.push_back( ss.str() ); - cargs.push_back( std::vector< CVC4::Type >() ); - pcs.push_back(nullptr); - weights.push_back(-1); + cnames[i].push_back(ss.str()); + cargs[i].push_back(std::vector<Type>()); + pcs[i].push_back(nullptr); + weights[i].push_back(-1); } - //ITE - CVC4::Kind k = kind::ITE; + // ITE + Kind k = ITE; Trace("sygus-grammar-def") << "...add for " << k << std::endl; ops[i].push_back(nm->operatorOf(k).toExpr()); - cnames.push_back( kind::kindToString(k) ); - cargs.push_back( std::vector< CVC4::Type >() ); - cargs.back().push_back(unres_bt); - cargs.back().push_back(unres_t); - cargs.back().push_back(unres_t); - pcs.push_back(nullptr); - weights.push_back(-1); + cnames[i].push_back(kindToString(k)); + cargs[i].push_back(std::vector<Type>()); + cargs[i].back().push_back(unres_bt); + cargs[i].back().push_back(unres_t); + cargs[i].back().push_back(unres_t); + pcs[i].push_back(nullptr); + weights[i].push_back(-1); if (types[i].isReal()) { @@ -521,16 +540,17 @@ void CegGrammarConstructor::mkSygusDefaultGrammar( Kind k = j == 0 ? PLUS : MINUS; Trace("sygus-grammar-def") << "...add for " << k << std::endl; ops[i].push_back(nm->operatorOf(k).toExpr()); - cnames.push_back(kind::kindToString(k)); - cargs.push_back(std::vector<CVC4::Type>()); - cargs.back().push_back(unres_t); - cargs.back().push_back(unres_t); - pcs.push_back(nullptr); - weights.push_back(-1); + cnames[i].push_back(kindToString(k)); + cargs[i].push_back(std::vector<Type>()); + cargs[i].back().push_back(unres_t); + cargs[i].back().push_back(unres_t); + pcs[i].push_back(nullptr); + weights[i].push_back(-1); } if (!types[i].isInteger()) { - Trace("sygus-grammar-def") << "...Dedicate to Real\n"; + Trace("sygus-grammar-def") + << " ...create auxiliary Positive Integers grammar\n"; /* Creating type for positive integers */ std::stringstream ss; ss << fun << "_PosInt"; @@ -546,7 +566,8 @@ void CegGrammarConstructor::mkSygusDefaultGrammar( /* Add operator 1 */ Trace("sygus-grammar-def") << "\t...add for 1 to Pos_Int\n"; ops_pos_int.push_back(nm->mkConst(Rational(1)).toExpr()); - ss << "_1"; + ss.str(""); + ss << "1"; cnames_pos_int.push_back(ss.str()); cargs_pos_int.push_back(std::vector<Type>()); /* Add operator PLUS */ @@ -558,23 +579,23 @@ void CegGrammarConstructor::mkSygusDefaultGrammar( cargs_pos_int.back().push_back(unres_pos_int_t); cargs_pos_int.back().push_back(unres_pos_int_t); datatypes.back().setSygus(types[i].toType(), bvl.toExpr(), true, true); - for (unsigned j = 0; j < ops_pos_int.size(); j++) + for (unsigned j = 0, size_j = ops_pos_int.size(); j < size_j; ++j) { datatypes.back().addSygusConstructor( ops_pos_int[j], cnames_pos_int[j], cargs_pos_int[j]); } Trace("sygus-grammar-def") - << "...built datatype " << datatypes.back() << " "; + << " ...built datatype " << datatypes.back() << " "; /* Adding division at root */ k = DIVISION; Trace("sygus-grammar-def") << "\t...add for " << k << std::endl; ops[i].push_back(nm->operatorOf(k).toExpr()); - cnames.push_back(kindToString(k)); - cargs.push_back(std::vector<Type>()); - cargs.back().push_back(unres_t); - cargs.back().push_back(unres_pos_int_t); - pcs.push_back(nullptr); - weights.push_back(-1); + cnames[i].push_back(kindToString(k)); + cargs[i].push_back(std::vector<Type>()); + cargs[i].back().push_back(unres_t); + cargs[i].back().push_back(unres_pos_int_t); + pcs[i].push_back(nullptr); + weights[i].push_back(-1); } } else if (types[i].isBitVector()) @@ -585,11 +606,11 @@ void CegGrammarConstructor::mkSygusDefaultGrammar( { Trace("sygus-grammar-def") << "...add for " << k << std::endl; ops[i].push_back(nm->operatorOf(k).toExpr()); - cnames.push_back(kindToString(k)); - cargs.push_back(std::vector<Type>()); - cargs.back().push_back(unres_t); - pcs.push_back(nullptr); - weights.push_back(-1); + cnames[i].push_back(kindToString(k)); + cargs[i].push_back(std::vector<Type>()); + cargs[i].back().push_back(unres_t); + pcs[i].push_back(nullptr); + weights[i].push_back(-1); } // binary apps std::vector<Kind> bin_kinds = {BITVECTOR_AND, @@ -609,56 +630,65 @@ void CegGrammarConstructor::mkSygusDefaultGrammar( { Trace("sygus-grammar-def") << "...add for " << k << std::endl; ops[i].push_back(nm->operatorOf(k).toExpr()); - cnames.push_back(kindToString(k)); - cargs.push_back(std::vector<Type>()); - cargs.back().push_back(unres_t); - cargs.back().push_back(unres_t); - pcs.push_back(nullptr); - weights.push_back(-1); + cnames[i].push_back(kindToString(k)); + cargs[i].push_back(std::vector<Type>()); + cargs[i].back().push_back(unres_t); + cargs[i].back().push_back(unres_t); + pcs[i].push_back(nullptr); + weights[i].push_back(-1); } } else if (types[i].isDatatype()) { Trace("sygus-grammar-def") << "...add for constructors" << std::endl; - const Datatype& dt = ((DatatypeType)types[i].toType()).getDatatype(); - for( unsigned k=0; k<dt.getNumConstructors(); k++ ){ + const Datatype& dt = types[i].getDatatype(); + for (unsigned k = 0, size_k = dt.getNumConstructors(); k < size_k; ++k) + { Trace("sygus-grammar-def") << "...for " << dt[k].getName() << std::endl; ops[i].push_back( dt[k].getConstructor() ); - cnames.push_back( dt[k].getName() ); - cargs.push_back( std::vector< CVC4::Type >() ); - for( unsigned j=0; j<dt[k].getNumArgs(); j++ ){ - TypeNode crange = TypeNode::fromType( ((SelectorType)dt[k][j].getType()).getRangeType() ); - //Assert( type_to_unres.find(crange)!=type_to_unres.end() ); - cargs.back().push_back( type_to_unres[crange] ); + cnames[i].push_back(dt[k].getName()); + cargs[i].push_back(std::vector<Type>()); + Trace("sygus-grammar-def") << "...add for selectors" << std::endl; + for (unsigned j = 0, size_j = dt[k].getNumArgs(); j < size_j; ++j) + { + Trace("sygus-grammar-def") + << "...for " << dt[k][j].getName() << std::endl; + TypeNode crange = TypeNode::fromType( + static_cast<SelectorType>(dt[k][j].getType()).getRangeType()); + Assert(type_to_unres.find(crange) != type_to_unres.end()); + cargs[i].back().push_back(type_to_unres[crange]); + // add to the selector type the selector operator + + Assert(std::find(types.begin(), types.end(), crange) != types.end()); + unsigned i_selType = std::distance( + types.begin(), std::find(types.begin(), types.end(), crange)); + TypeNode arg_type = TypeNode::fromType( + static_cast<SelectorType>(dt[k][j].getType()).getDomain()); + ops[i_selType].push_back(dt[k][j].getSelector()); + cnames[i_selType].push_back(dt[k][j].getName()); + cargs[i_selType].push_back(std::vector<Type>()); + Assert(type_to_unres.find(arg_type) != type_to_unres.end()); + cargs[i_selType].back().push_back(type_to_unres[arg_type]); + pcs[i_selType].push_back(nullptr); + weights[i_selType].push_back(-1); } - pcs.push_back(nullptr); - weights.push_back(-1); + pcs[i].push_back(nullptr); + weights[i].push_back(-1); } }else{ std::stringstream sserr; sserr << "No implementation for default Sygus grammar of type " << types[i] << std::endl; throw LogicException(sserr.str()); } - //add for all selectors to this type - if( !sels[types[i]].empty() ){ - Trace("sygus-grammar-def") << "...add for selectors" << std::endl; - for( unsigned j=0; j<sels[types[i]].size(); j++ ){ - Trace("sygus-grammar-def") << "...for " << sels[types[i]][j].getName() << std::endl; - TypeNode arg_type = TypeNode::fromType( ((SelectorType)sels[types[i]][j].getType()).getDomain() ); - ops[i].push_back( sels[types[i]][j].getSelector() ); - cnames.push_back( sels[types[i]][j].getName() ); - cargs.push_back( std::vector< CVC4::Type >() ); - //Assert( type_to_unres.find(arg_type)!=type_to_unres.end() ); - cargs.back().push_back( type_to_unres[arg_type] ); - pcs.push_back(nullptr); - weights.push_back(-1); - } - } + } + // make datatypes + for (unsigned i = 0, size = types.size(); i < size; ++i) + { Trace("sygus-grammar-def") << "...make datatype " << datatypes[i] << std::endl; datatypes[i].setSygus( types[i].toType(), bvl.toExpr(), true, true ); std::map<TypeNode, std::vector<Node>>::iterator itexc = exc_cons.find(types[i]); - for (unsigned j = 0, size = ops[i].size(); j < size; j++) + for (unsigned j = 0, size = ops[i].size(); j < size; ++j) { // add the constructor if it is not excluded Node opn = Node::fromExpr(ops[i][j]); @@ -667,12 +697,10 @@ void CegGrammarConstructor::mkSygusDefaultGrammar( == itexc->second.end()) { datatypes[i].addSygusConstructor( - ops[i][j], cnames[j], cargs[j], pcs[j], weights[j]); + ops[i][j], cnames[i][j], cargs[i][j], pcs[i][j], weights[i][j]); } } - Trace("sygus-grammar-def") - << "...built datatype " << datatypes[i] << " "; - //sorts.push_back( types[i] ); + Trace("sygus-grammar-def") << "...built datatype " << datatypes[i] << " "; //set start index if applicable if( types[i]==range ){ startIndex = i; @@ -683,94 +711,96 @@ void CegGrammarConstructor::mkSygusDefaultGrammar( TypeNode btype = nm->booleanType(); datatypes.push_back(Datatype(dbname)); ops.push_back(std::vector<Expr>()); - std::vector<std::string> cnames; - std::vector<std::vector< Type > > cargs; - /* Print callbacks for each constructor */ - std::vector<std::shared_ptr<SygusPrintCallback>> pcs; - /* Weights for each constructor */ - std::vector<int> weights; + cnames.push_back(std::vector<std::string>()); + cargs.push_back(std::vector<std::vector<Type>>()); + pcs.push_back(std::vector<std::shared_ptr<SygusPrintCallback>>()); + weights.push_back(std::vector<int>()); Trace("sygus-grammar-def") << "Make grammar for " << btype << " " << datatypes.back() << std::endl; //add variables - for( unsigned i=0; i<sygus_vars.size(); i++ ){ + for (unsigned i = 0, size = sygus_vars.size(); i < size; ++i) + { if( sygus_vars[i].getType().isBoolean() ){ std::stringstream ss; ss << sygus_vars[i]; Trace("sygus-grammar-def") << "...add for variable " << ss.str() << std::endl; ops.back().push_back( sygus_vars[i].toExpr() ); - cnames.push_back( ss.str() ); - cargs.push_back( std::vector< CVC4::Type >() ); - pcs.push_back(nullptr); - weights.push_back(1); + cnames.back().push_back(ss.str()); + cargs.back().push_back(std::vector<Type>()); + pcs.back().push_back(nullptr); + // make boolean variables weight as non-nullary constructors + weights.back().push_back(1); } } - //add constants + // add constants std::vector<Node> consts; mkSygusConstantsForType(btype, consts); - for (unsigned j = 0; j < consts.size(); j++) + for (unsigned i = 0, size = consts.size(); i < size; ++i) { std::stringstream ss; - ss << consts[j]; + ss << consts[i]; Trace("sygus-grammar-def") << "...add for constant " << ss.str() << std::endl; - ops.back().push_back(consts[j].toExpr()); - cnames.push_back(ss.str()); - cargs.push_back(std::vector<CVC4::Type>()); - pcs.push_back(nullptr); - weights.push_back(-1); + ops.back().push_back(consts[i].toExpr()); + cnames.back().push_back(ss.str()); + cargs.back().push_back(std::vector<Type>()); + pcs.back().push_back(nullptr); + weights.back().push_back(-1); } - //add predicates for types - for( unsigned i=0; i<types.size(); i++ ){ + // add predicates for types + for (unsigned i = 0, size = types.size(); i < size; ++i) + { Trace("sygus-grammar-def") << "...add predicates for " << types[i] << std::endl; //add equality per type - CVC4::Kind k = kind::EQUAL; + Kind k = EQUAL; Trace("sygus-grammar-def") << "...add for " << k << std::endl; ops.back().push_back(nm->operatorOf(k).toExpr()); std::stringstream ss; - ss << kind::kindToString(k) << "_" << types[i]; - cnames.push_back(ss.str()); - cargs.push_back( std::vector< CVC4::Type >() ); - cargs.back().push_back(unres_types[i]); - cargs.back().push_back(unres_types[i]); - pcs.push_back(nullptr); - weights.push_back(-1); - //type specific predicates + ss << kindToString(k) << "_" << types[i]; + cnames.back().push_back(ss.str()); + cargs.back().push_back(std::vector<Type>()); + cargs.back().back().push_back(unres_types[i]); + cargs.back().back().push_back(unres_types[i]); + pcs.back().push_back(nullptr); + weights.back().push_back(-1); + // type specific predicates if (types[i].isReal()) { - CVC4::Kind k = kind::LEQ; + Kind k = LEQ; Trace("sygus-grammar-def") << "...add for " << k << std::endl; ops.back().push_back(nm->operatorOf(k).toExpr()); - cnames.push_back(kind::kindToString(k)); - cargs.push_back( std::vector< CVC4::Type >() ); - cargs.back().push_back(unres_types[i]); - cargs.back().push_back(unres_types[i]); - pcs.push_back(nullptr); - weights.push_back(-1); + cnames.back().push_back(kindToString(k)); + cargs.back().push_back(std::vector<Type>()); + cargs.back().back().push_back(unres_types[i]); + cargs.back().back().push_back(unres_types[i]); + pcs.back().push_back(nullptr); + weights.back().push_back(-1); } else if (types[i].isBitVector()) { Kind k = BITVECTOR_ULT; Trace("sygus-grammar-def") << "...add for " << k << std::endl; ops.back().push_back(nm->operatorOf(k).toExpr()); - cnames.push_back(kindToString(k)); - cargs.push_back(std::vector<Type>()); - cargs.back().push_back(unres_types[i]); - cargs.back().push_back(unres_types[i]); - pcs.push_back(nullptr); - weights.push_back(-1); + cnames.back().push_back(kindToString(k)); + cargs.back().push_back(std::vector<Type>()); + cargs.back().back().push_back(unres_types[i]); + cargs.back().back().push_back(unres_types[i]); + pcs.back().push_back(nullptr); + weights.back().push_back(-1); } else if (types[i].isDatatype()) { //add for testers Trace("sygus-grammar-def") << "...add for testers" << std::endl; - const Datatype& dt = ((DatatypeType)types[i].toType()).getDatatype(); - for( unsigned k=0; k<dt.getNumConstructors(); k++ ){ + const Datatype& dt = types[i].getDatatype(); + for (unsigned k = 0, size_k = dt.getNumConstructors(); k < size_k; ++k) + { Trace("sygus-grammar-def") << "...for " << dt[k].getTesterName() << std::endl; ops.back().push_back(dt[k].getTester()); - cnames.push_back(dt[k].getTesterName()); - cargs.push_back( std::vector< CVC4::Type >() ); - cargs.back().push_back(unres_types[i]); - pcs.push_back(nullptr); - weights.push_back(-1); + cnames.back().push_back(dt[k].getTesterName()); + cargs.back().push_back(std::vector<Type>()); + cargs.back().back().push_back(unres_types[i]); + pcs.back().push_back(nullptr); + weights.back().push_back(-1); } } } @@ -790,19 +820,19 @@ void CegGrammarConstructor::mkSygusDefaultGrammar( } Trace("sygus-grammar-def") << "...add for " << k << std::endl; ops.back().push_back(nm->operatorOf(k).toExpr()); - cnames.push_back(kindToString(k)); - cargs.push_back(std::vector<CVC4::Type>()); - cargs.back().push_back(unres_bt); + cnames.back().push_back(kindToString(k)); + cargs.back().push_back(std::vector<Type>()); + cargs.back().back().push_back(unres_bt); if (k != NOT) { - cargs.back().push_back(unres_bt); + cargs.back().back().push_back(unres_bt); if (k == ITE) { - cargs.back().push_back(unres_bt); + cargs.back().back().push_back(unres_bt); } } - pcs.push_back(nullptr); - weights.push_back(-1); + pcs.back().push_back(nullptr); + weights.back().push_back(-1); } } if( range==btype ){ @@ -810,15 +840,19 @@ void CegGrammarConstructor::mkSygusDefaultGrammar( } Trace("sygus-grammar-def") << "...make datatype " << datatypes.back() << std::endl; datatypes.back().setSygus( btype.toType(), bvl.toExpr(), true, true ); - for( unsigned j=0; j<ops.back().size(); j++ ){ - datatypes.back().addSygusConstructor( - ops.back()[j], cnames[j], cargs[j], pcs[j], weights[j]); + for (unsigned i = 0, size = ops.back().size(); i < size; ++i) + { + datatypes.back().addSygusConstructor(ops.back()[i], + cnames.back()[i], + cargs.back()[i], + pcs.back()[i], + weights.back()[i]); } - //sorts.push_back( btype ); + Trace("sygus-grammar-def") << "...built datatype " << datatypes.back() << " "; Trace("sygus-grammar-def") << "...finished make default grammar for " << fun << " " << range << std::endl; - + // make first datatype be the top level datatype if( startIndex>0 ){ - CVC4::Datatype tmp_dt = datatypes[0]; + Datatype tmp_dt = datatypes[0]; datatypes[0] = datatypes[startIndex]; datatypes[startIndex] = tmp_dt; } diff --git a/src/theory/quantifiers/sygus/sygus_grammar_cons.h b/src/theory/quantifiers/sygus/sygus_grammar_cons.h index 0c5b67656..3afc4c689 100644 --- a/src/theory/quantifiers/sygus/sygus_grammar_cons.h +++ b/src/theory/quantifiers/sygus/sygus_grammar_cons.h @@ -131,7 +131,8 @@ public: // helper for mkSygusDefaultGrammar (makes unresolved type for mutually recursive datatype construction) static TypeNode mkUnresolvedType(const std::string& name, std::set<Type>& unres); // collect the list of types that depend on type range - static void collectSygusGrammarTypesFor( TypeNode range, std::vector< TypeNode >& types, std::map< TypeNode, std::vector< DatatypeConstructorArg > >& sels ); + static void collectSygusGrammarTypesFor(TypeNode range, + std::vector<TypeNode>& types); /** helper function for function mkSygusDefaultType * Collects a set of mutually recursive datatypes "datatypes" corresponding to * encoding type "range" to SyGuS. diff --git a/src/theory/quantifiers/sygus/sygus_pbe.cpp b/src/theory/quantifiers/sygus/sygus_pbe.cpp index b49c29c53..ee7247121 100644 --- a/src/theory/quantifiers/sygus/sygus_pbe.cpp +++ b/src/theory/quantifiers/sygus/sygus_pbe.cpp @@ -179,7 +179,6 @@ bool SygusPbe::initialize(Node n, return false; } } - bool isActiveGen = options::sygusActiveGenMode() != SYGUS_ACTIVE_GEN_NONE; for (const Node& c : candidates) { Assert(d_examples.find(c) != d_examples.end()); @@ -203,7 +202,7 @@ bool SygusPbe::initialize(Node n, for (const Node& e : d_candidate_to_enum[c]) { TypeNode etn = e.getType(); - d_tds->registerEnumerator(e, c, d_parent, true, false, isActiveGen); + d_tds->registerEnumerator(e, c, d_parent, ROLE_ENUM_POOL, false); d_enum_to_candidate[e] = c; TNode te = e; // initialize static symmetry breaking lemmas for it @@ -229,13 +228,24 @@ bool SygusPbe::initialize(Node n, { lem = lem.substitute(tsp, te); } - disj.push_back(lem); + if (std::find(disj.begin(), disj.end(), lem) == disj.end()) + { + disj.push_back(lem); + } } } + // add its active guard + Node ag = d_tds->getActiveGuardForEnumerator(e); + Assert(!ag.isNull()); + disj.push_back(ag.negate()); Node lem = disj.size() == 1 ? disj[0] : nm->mkNode(OR, disj); Trace("sygus-pbe") << " static redundant op lemma : " << lem << std::endl; - lemmas.push_back(lem); + // Register as a symmetry breaking lemma with the term database. + // This will either be processed via a lemma on the output channel + // of the sygus extension of the datatypes solver, or internally + // encoded as a constraint to an active enumerator. + d_tds->registerSymBreakLemma(e, lem, etn, 0, false); } } Trace("sygus-pbe") << "Initialize " << d_examples[c].size() diff --git a/src/theory/quantifiers/sygus/synth_conjecture.cpp b/src/theory/quantifiers/sygus/synth_conjecture.cpp index 21079aedc..2bfde2d80 100644 --- a/src/theory/quantifiers/sygus/synth_conjecture.cpp +++ b/src/theory/quantifiers/sygus/synth_conjecture.cpp @@ -346,14 +346,17 @@ bool SynthConjecture::doCheck(std::vector<Node>& lems) { // get the model value of the relevant terms from the master module std::vector<Node> enum_values; - bool fullModel = getEnumeratedValues(terms, enum_values); + bool activeIncomplete = false; + bool fullModel = getEnumeratedValues(terms, enum_values, activeIncomplete); // if the master requires a full model and the model is partial, we fail if (!d_master->allowPartialModel() && !fullModel) { // we retain the values in d_ev_active_gen_waiting Trace("cegqi-engine") << "...partial model, fail." << std::endl; - return true; + // if we are partial due to an active enumerator, we may still succeed + // on the next call + return !activeIncomplete; } // the waiting values are passed to the module below, clear d_ev_active_gen_waiting.clear(); @@ -396,7 +399,7 @@ bool SynthConjecture::doCheck(std::vector<Node>& lems) if (emptyModel) { Trace("cegqi-engine") << "...empty model, fail." << std::endl; - return true; + return !activeIncomplete; } Assert(candidate_values.empty()); constructed_cand = d_master->constructCandidates( @@ -650,7 +653,8 @@ void SynthConjecture::preregisterConjecture(Node q) } bool SynthConjecture::getEnumeratedValues(std::vector<Node>& n, - std::vector<Node>& v) + std::vector<Node>& v, + bool& activeIncomplete) { std::vector<Node> ncheck = n; n.clear(); @@ -670,7 +674,7 @@ bool SynthConjecture::getEnumeratedValues(std::vector<Node>& n, continue; } } - Node nv = getEnumeratedValue(e); + Node nv = getEnumeratedValue(e, activeIncomplete); n.push_back(e); v.push_back(nv); ret = ret && !nv.isNull(); @@ -692,42 +696,50 @@ class EnumValGeneratorBasic : public EnumValGenerator /** initialize (do nothing) */ void initialize(Node e) override {} /** initialize (do nothing) */ - void addValue(Node v) override {} + void addValue(Node v) override { d_currTerm = *d_te; } /** * Get next returns the next (T-rewriter-unique) value based on the type * enumerator. */ - Node getNext() override + bool increment() override { + ++d_te; if (d_te.isFinished()) { - return Node::null(); + d_currTerm = Node::null(); + return false; } - Node next = *d_te; - ++d_te; - Node nextb = d_tds->sygusToBuiltin(next); + d_currTerm = *d_te; if (options::sygusSymBreakDynamic()) { + Node nextb = d_tds->sygusToBuiltin(d_currTerm); nextb = d_tds->getExtRewriter()->extendedRewrite(nextb); + if (d_cache.find(nextb) == d_cache.end()) + { + d_cache.insert(nextb); + // only return the current term if not unique + } + else + { + d_currTerm = Node::null(); + } } - if (d_cache.find(nextb) == d_cache.end()) - { - d_cache.insert(nextb); - return next; - } - return getNext(); + return true; } - + /** get the current term */ + Node getCurrent() override { return d_currTerm; } private: /** pointer to term database sygus */ TermDbSygus* d_tds; /** the type enumerator */ TypeEnumerator d_te; + /** the current term */ + Node d_currTerm; /** cache of (enumerated) builtin values we have enumerated so far */ std::unordered_set<Node, NodeHashFunction> d_cache; }; -Node SynthConjecture::getEnumeratedValue(Node e) +Node SynthConjecture::getEnumeratedValue(Node e, bool& activeIncomplete) { bool isEnum = d_tds->isEnumerator(e); @@ -761,15 +773,18 @@ Node SynthConjecture::getEnumeratedValue(Node e) else { // Actively-generated enumerators are currently either variable agnostic - // or basic. + // or basic. The auto mode always prefers the optimized enumerator over + // the basic one. Assert(d_tds->isBasicEnumerator(e)); - if (options::sygusActiveGenMode() == SYGUS_ACTIVE_GEN_ENUM) + if (options::sygusActiveGenMode() == SYGUS_ACTIVE_GEN_ENUM_BASIC) { - d_evg[e].reset(new SygusEnumerator(d_tds, this)); + d_evg[e].reset(new EnumValGeneratorBasic(d_tds, e.getType())); } else { - d_evg[e].reset(new EnumValGeneratorBasic(d_tds, e.getType())); + Assert(options::sygusActiveGenMode() == SYGUS_ACTIVE_GEN_ENUM + || options::sygusActiveGenMode() == SYGUS_ACTIVE_GEN_AUTO); + d_evg[e].reset(new SygusEnumerator(d_tds, this)); } } Trace("sygus-active-gen") @@ -790,6 +805,7 @@ Node SynthConjecture::getEnumeratedValue(Node e) // Check if there is an (abstract) value absE we were actively generating // values based on. Node absE = d_ev_curr_active_gen[e]; + bool firstTime = false; if (absE.isNull()) { // None currently exist. The next abstract value is the model value for e. @@ -804,9 +820,22 @@ Node SynthConjecture::getEnumeratedValue(Node e) } d_ev_curr_active_gen[e] = absE; iteg->second->addValue(absE); + firstTime = true; } - Node v = iteg->second->getNext(); - if (v.isNull()) + bool inc = true; + if (!firstTime) + { + inc = iteg->second->increment(); + } + Node v; + if (inc) + { + v = iteg->second->getCurrent(); + } + Trace("sygus-active-gen-debug") << "...generated " << v + << ", with increment success : " << inc + << std::endl; + if (!inc) { // No more concrete values generated from absE. NodeManager* nm = NodeManager::currentNM(); @@ -852,7 +881,14 @@ Node SynthConjecture::getEnumeratedValue(Node e) else { // We are waiting to send e -> v to the module that requested it. - d_ev_active_gen_waiting[e] = v; + if (v.isNull()) + { + activeIncomplete = true; + } + else + { + d_ev_active_gen_waiting[e] = v; + } if (Trace.isOn("sygus-active-gen")) { Trace("sygus-active-gen") << "Active-gen : " << e << " : "; diff --git a/src/theory/quantifiers/sygus/synth_conjecture.h b/src/theory/quantifiers/sygus/synth_conjecture.h index ef1b4459f..3a43eb83d 100644 --- a/src/theory/quantifiers/sygus/synth_conjecture.h +++ b/src/theory/quantifiers/sygus/synth_conjecture.h @@ -49,8 +49,14 @@ class EnumValGenerator virtual void initialize(Node e) = 0; /** Inform this generator that abstract value v was enumerated. */ virtual void addValue(Node v) = 0; - /** Get the next concrete value generated by this class. */ - virtual Node getNext() = 0; + /** + * Increment this value generator. If this returns false, then we are out of + * values. If this returns true, getCurrent(), if non-null, returns the + * current term. + */ + virtual bool increment() = 0; + /** Get the current concrete value generated by this class. */ + virtual Node getCurrent() = 0; }; /** a synthesis conjecture @@ -193,15 +199,25 @@ class SynthConjecture * Get model values for terms n, store in vector v. This method returns true * if and only if all values added to v are non-null. * + * The argument activeIncomplete indicates whether n contains an active + * enumerator that is currently not finished enumerating values, but returned + * null on a call to getEnumeratedValue. This value is used for determining + * whether we should call getEnumeratedValues again within a call to + * SynthConjecture::check. + * * It removes terms from n that correspond to "inactive" enumerators, that * is, enumerators whose values have been exhausted. */ - bool getEnumeratedValues(std::vector<Node>& n, std::vector<Node>& v); + bool getEnumeratedValues(std::vector<Node>& n, + std::vector<Node>& v, + bool& activeIncomplete); /** * Get model value for term n. If n has a value that was excluded by - * datatypes sygus symmetry breaking, this method returns null. + * datatypes sygus symmetry breaking, this method returns null. It sets + * activeIncomplete to true if there is an actively-generated enumerator whose + * current value is null but it has not finished generating values. */ - Node getEnumeratedValue(Node n); + Node getEnumeratedValue(Node n, bool& activeIncomplete); /** enumerator generators for each actively-generated enumerator */ std::map<Node, std::unique_ptr<EnumValGenerator> > d_evg; /** diff --git a/src/theory/quantifiers/sygus/term_database_sygus.cpp b/src/theory/quantifiers/sygus/term_database_sygus.cpp index 435e1a00f..9198f7e56 100644 --- a/src/theory/quantifiers/sygus/term_database_sygus.cpp +++ b/src/theory/quantifiers/sygus/term_database_sygus.cpp @@ -58,6 +58,19 @@ void TypeNodeIdTrie::assignIds(std::map<Node, unsigned>& assign, } } +std::ostream& operator<<(std::ostream& os, EnumeratorRole r) +{ + switch (r) + { + case ROLE_ENUM_POOL: os << "POOL"; break; + case ROLE_ENUM_SINGLE_SOLUTION: os << "SINGLE_SOLUTION"; break; + case ROLE_ENUM_MULTI_SOLUTION: os << "MULTI_SOLUTION"; break; + case ROLE_ENUM_CONSTRAINED: os << "CONSTRAINED"; break; + default: os << "enum_" << static_cast<unsigned>(r); break; + } + return os; +} + TermDbSygus::TermDbSygus(context::Context* c, QuantifiersEngine* qe) : d_quantEngine(qe), d_syexp(new SygusExplain(this)), @@ -454,9 +467,8 @@ void TermDbSygus::registerSygusType( TypeNode tn ) { void TermDbSygus::registerEnumerator(Node e, Node f, SynthConjecture* conj, - bool mkActiveGuard, - bool useSymbolicCons, - bool isActiveGen) + EnumeratorRole erole, + bool useSymbolicCons) { if (d_enum_to_conjecture.find(e) != d_enum_to_conjecture.end()) { @@ -470,13 +482,6 @@ void TermDbSygus::registerEnumerator(Node e, d_enum_to_conjecture[e] = conj; d_enum_to_synth_fun[e] = f; NodeManager* nm = NodeManager::currentNM(); - if( mkActiveGuard ){ - // make the guard - Node ag = nm->mkSkolem("eG", nm->booleanType()); - // must ensure it is a literal immediately here - ag = d_quantEngine->getValuation().ensureLiteral(ag); - d_enum_to_active_guard[e] = ag; - } Trace("sygus-db") << " registering symmetry breaking clauses..." << std::endl; @@ -554,6 +559,66 @@ void TermDbSygus::registerEnumerator(Node e, } Trace("sygus-db") << " ...finished" << std::endl; + // determine if we are actively-generated + bool isActiveGen = false; + if (options::sygusActiveGenMode() != SYGUS_ACTIVE_GEN_NONE) + { + if (erole == ROLE_ENUM_MULTI_SOLUTION || erole == ROLE_ENUM_CONSTRAINED) + { + // If the enumerator is a solution for a conjecture with multiple + // functions, we do not use active generation. If we did, we would have to + // generate a "product" of two actively-generated enumerators. That is, + // given a conjecture with two functions-to-synthesize with enumerators + // e_f and e_g, and if these enumerators generated: + // e_f -> t1, ..., tn + // e_g -> s1, ..., sm + // The sygus module in charge of this conjecture would expect + // constructCandidates calls of the form + // (e_f,e_g) -> (ti, sj) + // for each i,j. We instead use passive enumeration in this case. + // + // If the enumerator is constrained, it cannot be actively generated. + } + else if (erole == ROLE_ENUM_POOL) + { + // If the enumerator is used for generating a pool of values, we always + // use active generation. + isActiveGen = true; + } + else if (erole == ROLE_ENUM_SINGLE_SOLUTION) + { + // If the enumerator is the single function-to-synthesize, if auto is + // enabled, we infer whether it is better to enable active generation. + if (options::sygusActiveGenMode() == SYGUS_ACTIVE_GEN_AUTO) + { + // We use active generation if the grammar of the enumerator does not + // have ITE and is not Boolean. Experimentally, it is better to + // use passive generation for these cases since it enables useful + // search space pruning techniques, e.g. evaluation unfolding, + // conjecture-specific symmetry breaking. Also, if sygus-stream is + // enabled, we always use active generation, since the use cases of + // sygus stream are to find many solutions to an easy problem, where + // the bottleneck often becomes the large number of "exclude the current + // solution" clauses. + const Datatype& dt = et.getDatatype(); + if (options::sygusStream() + || (!hasKind(et, ITE) && !dt.getSygusType().isBoolean())) + { + isActiveGen = true; + } + } + else + { + isActiveGen = true; + } + } + else + { + Unreachable("Unknown enumerator mode in registerEnumerator"); + } + } + Trace("sygus-db") << "isActiveGen for " << e << ", role = " << erole + << " returned " << isActiveGen << std::endl; // Currently, actively-generated enumerators are either basic or variable // agnostic. bool isVarAgnostic = @@ -607,6 +672,22 @@ void TermDbSygus::registerEnumerator(Node e, } d_enum_active_gen[e] = isActiveGen; d_enum_basic[e] = isActiveGen && !isVarAgnostic; + + // We make an active guard if we will be explicitly blocking solutions for + // the enumerator. This is the case if the role of the enumerator is to + // populate a pool of terms, or (some cases) of when it is actively generated. + if (isActiveGen || erole == ROLE_ENUM_POOL) + { + // make the guard + Node ag = nm->mkSkolem("eG", nm->booleanType()); + // must ensure it is a literal immediately here + ag = d_quantEngine->getValuation().ensureLiteral(ag); + // must ensure that it is asserted as a literal before we begin solving + Node lem = nm->mkNode(OR, ag, ag.negate()); + d_quantEngine->getOutputChannel().requirePhase(ag, true); + d_quantEngine->getOutputChannel().lemma(lem); + d_enum_to_active_guard[e] = ag; + } } bool TermDbSygus::isEnumerator(Node e) const @@ -694,14 +775,13 @@ void TermDbSygus::getEnumerators(std::vector<Node>& mts) } } -void TermDbSygus::registerSymBreakLemma(Node e, - Node lem, - TypeNode tn, - unsigned sz) +void TermDbSygus::registerSymBreakLemma( + Node e, Node lem, TypeNode tn, unsigned sz, bool isTempl) { d_enum_to_sb_lemmas[e].push_back(lem); d_sb_lemma_to_type[lem] = tn; d_sb_lemma_to_size[lem] = sz; + d_sb_lemma_to_isTempl[lem] = isTempl; } bool TermDbSygus::hasSymBreakLemmas(std::vector<Node>& enums) const @@ -740,6 +820,13 @@ unsigned TermDbSygus::getSizeForSymBreakLemma(Node lem) const return it->second; } +bool TermDbSygus::isSymBreakLemmaTemplate(Node lem) const +{ + std::map<Node, bool>::const_iterator it = d_sb_lemma_to_isTempl.find(lem); + Assert(it != d_sb_lemma_to_isTempl.end()); + return it->second; +} + void TermDbSygus::clearSymBreakLemmas(Node e) { d_enum_to_sb_lemmas.erase(e); } bool TermDbSygus::isRegistered(TypeNode tn) const @@ -756,9 +843,16 @@ void TermDbSygus::toStreamSygus(const char* c, Node n) { if (Trace.isOn(c)) { - std::stringstream ss; - Printer::getPrinter(options::outputLanguage())->toStreamSygus(ss, n); - Trace(c) << ss.str(); + if (n.isNull()) + { + Trace(c) << n; + } + else + { + std::stringstream ss; + Printer::getPrinter(options::outputLanguage())->toStreamSygus(ss, n); + Trace(c) << ss.str(); + } } } diff --git a/src/theory/quantifiers/sygus/term_database_sygus.h b/src/theory/quantifiers/sygus/term_database_sygus.h index 713e322a4..7a522ded6 100644 --- a/src/theory/quantifiers/sygus/term_database_sygus.h +++ b/src/theory/quantifiers/sygus/term_database_sygus.h @@ -48,6 +48,23 @@ class TypeNodeIdTrie void assignIds(std::map<Node, unsigned>& assign, unsigned& idCount); }; +/** role for registering an enumerator */ +enum EnumeratorRole +{ + /** The enumerator populates a pool of terms (e.g. for PBE). */ + ROLE_ENUM_POOL, + /** The enumerator is the single solution of the problem. */ + ROLE_ENUM_SINGLE_SOLUTION, + /** + * The enumerator is part of the solution of the problem (e.g. multiple + * functions to synthesize). + */ + ROLE_ENUM_MULTI_SOLUTION, + /** The enumerator must satisfy some set of constraints */ + ROLE_ENUM_CONSTRAINED, +}; +std::ostream& operator<<(std::ostream& os, EnumeratorRole r); + // TODO :issue #1235 split and document this class class TermDbSygus { public: @@ -80,29 +97,32 @@ class TermDbSygus { //------------------------------enumerators /** * Register a variable e that we will do enumerative search on. + * * conj : the conjecture that the enumeration of e is for. - * f : the synth-fun that the enumeration of e is for. - * mkActiveGuard : whether we want to make an active guard for e - * (see d_enum_to_active_guard), - * useSymbolicCons : whether we want model values for e to include symbolic - * constructors like the "any constant" variable. - * isActiveGen : if this flag is true, the enumerator will be - * actively-generated based on the mode specified by --sygus-active-gen. + * + * f : the synth-fun that the enumeration of e is for.Notice that enumerator + * e may not be one-to-one with f in synthesis-through-unification approaches + * (e.g. decision tree construction for PBE synthesis). + * + * erole : the role of this enumerator (see definition of EnumeratorRole). + * Depending on this and the policy for actively-generated enumerators + * (--sygus-active-gen), the enumerator may be "actively-generated". * For example, if --sygus-active-gen=var-agnostic, then the enumerator will * only generate values whose variables are in canonical order (only x1-x2 * and not x2-x1 will be generated, assuming x1 and x2 are in the same * "subclass", see getSubclassForVar). * - * Notice that enumerator e may not be one-to-one with f in - * synthesis-through-unification approaches (e.g. decision tree construction - * for PBE synthesis). + * useSymbolicCons : whether we want model values for e to include symbolic + * constructors like the "any constant" variable. + * + * An "active guard" may be allocated by this method for e based on erole + * and the policies for active generation. */ void registerEnumerator(Node e, Node f, SynthConjecture* conj, - bool mkActiveGuard = false, - bool useSymbolicCons = false, - bool isActiveGen = false); + EnumeratorRole erole, + bool useSymbolicCons = false); /** is e an enumerator registered with this class? */ bool isEnumerator(Node e) const; /** return the conjecture e is associated with */ @@ -150,12 +170,13 @@ class TermDbSygus { * * tn : the (sygus datatype) type that lem applies to, i.e. the * type of terms that lem blocks models for, - * sz : the minimum size of terms that the lem blocks. - * - * Notice that the symmetry breaking lemma template should be relative to x, - * where x is returned by the call to getFreeVar( tn, 0 ) in this class. + * sz : the minimum size of terms that the lem blocks, + * isTempl : if this flag is false, then lem is a (concrete) lemma. + * If this flag is true, then lem is a symmetry breaking lemma template + * over x, where x is returned by the call to getFreeVar( tn, 0 ). */ - void registerSymBreakLemma(Node e, Node lem, TypeNode tn, unsigned sz); + void registerSymBreakLemma( + Node e, Node lem, TypeNode tn, unsigned sz, bool isTempl = true); /** Has symmetry breaking lemmas been added for any enumerator? */ bool hasSymBreakLemmas(std::vector<Node>& enums) const; /** Get symmetry breaking lemmas @@ -168,6 +189,8 @@ class TermDbSygus { TypeNode getTypeForSymBreakLemma(Node lem) const; /** Get the minimum size of terms symmetry breaking lemma lem applies to */ unsigned getSizeForSymBreakLemma(Node lem) const; + /** Returns true if lem is a lemma template, false if lem is a lemma */ + bool isSymBreakLemmaTemplate(Node lem) const; /** Clear information about symmetry breaking lemmas for enumerator e */ void clearSymBreakLemmas(Node e); //------------------------------end enumerators @@ -324,6 +347,8 @@ class TermDbSygus { std::map<Node, TypeNode> d_sb_lemma_to_type; /** mapping from symmetry breaking lemmas to size */ std::map<Node, unsigned> d_sb_lemma_to_size; + /** mapping from symmetry breaking lemmas to whether they are templates */ + std::map<Node, bool> d_sb_lemma_to_isTempl; /** enumerators to whether they are actively-generated */ std::map<Node, bool> d_enum_active_gen; /** enumerators to whether they are variable agnostic */ diff --git a/src/theory/strings/theory_strings_preprocess.cpp b/src/theory/strings/theory_strings_preprocess.cpp index fcb02d058..a1b37e6fb 100644 --- a/src/theory/strings/theory_strings_preprocess.cpp +++ b/src/theory/strings/theory_strings_preprocess.cpp @@ -192,7 +192,10 @@ Node StringsPreprocess::simplify( Node t, std::vector< Node > &new_nodes ) { Node ud = nm->mkSkolem("Ud", nm->mkFunctionType(argTypes, nm->stringType())); - Node lem = n.eqNode(nm->mkNode(APPLY_UF, u, leni)); + Node lem = nm->mkNode(GEQ, leni, d_one); + conc.push_back(lem); + + lem = n.eqNode(nm->mkNode(APPLY_UF, u, leni)); conc.push_back(lem); lem = d_zero.eqNode(nm->mkNode(APPLY_UF, u, d_zero)); @@ -205,23 +208,26 @@ Node StringsPreprocess::simplify( Node t, std::vector< Node > &new_nodes ) { conc.push_back(lem); Node x = nm->mkBoundVar(nm->integerType()); + Node xPlusOne = nm->mkNode(PLUS, x, d_one); Node xbv = nm->mkNode(BOUND_VAR_LIST, x); Node g = nm->mkNode(AND, nm->mkNode(GEQ, x, d_zero), nm->mkNode(LT, x, leni)); Node udx = nm->mkNode(APPLY_UF, ud, x); Node ux = nm->mkNode(APPLY_UF, u, x); - Node ux1 = nm->mkNode(APPLY_UF, u, nm->mkNode(PLUS, x, d_one)); + Node ux1 = nm->mkNode(APPLY_UF, u, xPlusOne); Node c0 = nm->mkNode(STRING_CODE, nm->mkConst(String("0"))); Node c = nm->mkNode(MINUS, nm->mkNode(STRING_CODE, udx), c0); Node usx = nm->mkNode(APPLY_UF, us, x); - Node usx1 = nm->mkNode(APPLY_UF, us, nm->mkNode(PLUS, x, d_one)); + Node usx1 = nm->mkNode(APPLY_UF, us, xPlusOne); Node ten = nm->mkConst(Rational(10)); Node eqs = usx.eqNode(nm->mkNode(STRING_CONCAT, udx, usx1)); Node eq = ux1.eqNode(nm->mkNode(PLUS, c, nm->mkNode(MULT, ten, ux))); + Node leadingZeroPos = + nm->mkNode(AND, x.eqNode(d_zero), nm->mkNode(GT, leni, d_one)); Node cb = nm->mkNode( AND, - nm->mkNode(GEQ, c, nm->mkNode(ITE, x.eqNode(d_zero), d_one, d_zero)), + nm->mkNode(GEQ, c, nm->mkNode(ITE, leadingZeroPos, d_one, d_zero)), nm->mkNode(LT, c, ten)); lem = nm->mkNode(OR, g.negate(), nm->mkNode(AND, eqs, eq, cb)); @@ -236,12 +242,13 @@ Node StringsPreprocess::simplify( Node t, std::vector< Node > &new_nodes ) { // assert: // IF n>=0 // THEN: + // len( itost ) >= 1 ^ // n = U( len( itost ) ) ^ U( 0 ) = 0 ^ // "" = Us( len( itost ) ) ^ itost = Us( 0 ) ^ // forall x. (x>=0 ^ x < str.len(itost)) => // Us( x ) = Ud( x ) ++ Us( x+1 ) ^ // U( x+1 ) = (str.code( Ud( x ) )-48) + 10*U( x ) ^ - // ite( x=0, 49, 48 ) <= str.code( Ud( x ) ) < 58 + // ite( x=0 AND str.len(itost)>1, 49, 48 ) <= str.code( Ud( x ) ) < 58 // ELSE // itost = "" // thus: @@ -254,7 +261,8 @@ Node StringsPreprocess::simplify( Node t, std::vector< Node > &new_nodes ) { // str.to.int( str.substr( int.to.str( n ), 0, x ) ). For example, for // n=345, we have that U(1), U(2), U(3) = 3, 34, 345. // Above, we use str.code to map characters to their integer value, where - // note that str.code( "0" ) = 48. Further notice that ite( x=0, 49, 48 ) + // note that str.code( "0" ) = 48. Further notice that + // ite( x=0 AND str.len(itost)>1, 49, 48 ) // enforces that int.to.str( n ) has no leading zeroes. retNode = itost; } else if( t.getKind() == kind::STRING_STOI ) { diff --git a/src/theory/strings/theory_strings_rewriter.cpp b/src/theory/strings/theory_strings_rewriter.cpp index c90576726..aa5b616fe 100644 --- a/src/theory/strings/theory_strings_rewriter.cpp +++ b/src/theory/strings/theory_strings_rewriter.cpp @@ -4962,7 +4962,7 @@ std::pair<bool, std::vector<Node> > TheoryStringsRewriter::collectEmptyEqs( allEmptyEqs = false; } } - else + else if (x.getKind() == kind::AND) { for (const Node& c : x) { diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt index 5aea954e3..5304fcab5 100644 --- a/test/regress/CMakeLists.txt +++ b/test/regress/CMakeLists.txt @@ -157,6 +157,8 @@ set(regress_0_tests regress0/buggy-ite.smt2 regress0/bv/ackermann1.smt2 regress0/bv/ackermann2.smt2 + regress0/bv/ackermann3.smt2 + regress0/bv/ackermann4.smt2 regress0/bv/bool-to-bv.smt2 regress0/bv/bug260a.smt regress0/bv/bug260b.smt @@ -171,7 +173,8 @@ set(regress_0_tests regress0/bv/bv-options2.smt2 regress0/bv/bv-options3.smt2 regress0/bv/bv-options4.smt2 - regress0/bv/bv-to-bool.smt + regress0/bv/bv-to-bool1.smt + regress0/bv/bv-to-bool2.smt2 regress0/bv/bv2nat-ground-c.smt2 regress0/bv/bv2nat-simp-range.smt2 regress0/bv/bvmul-pow2-only.smt2 @@ -836,6 +839,7 @@ set(regress_0_tests regress0/strings/substr-rewrites.smt2 regress0/strings/type001.smt2 regress0/strings/unsound-0908.smt2 + regress0/strings/unsound-repl-rewrite.smt2 regress0/sygus/General_plus10.sy regress0/sygus/aig-si.sy regress0/sygus/c100.sy diff --git a/test/regress/README.md b/test/regress/README.md index d43ebf337..28ccfb96b 100644 --- a/test/regress/README.md +++ b/test/regress/README.md @@ -3,20 +3,10 @@ ## Regression Levels and Running Regression Tests CVC4's regression tests are divided into 5 levels (level 0 to 4). Higher -regression levels are reserved for longer running regressions. To run -regressions up to a certain level use `make regressX` where `X` designates the -level. `make regress` by default runs levels 0 and 1. On Travis, we only run -regression level 0 to keep the time short. During our nightly builds, we run -regression level 2. +regression levels are reserved for longer running regressions. -To only run some benchmarks, you can use the `TEST_REGEX` environment variable. -For example: - -``` -TEST_REGEX=quantifiers make regress0 -``` - -This runs regression tests from level 0 that have "quantifiers" in their name. +For running regressions tests, +see the [INSTALL](https://github.com/CVC4/CVC4/blob/master/INSTALL.md#testing-cvc4) file. By default, each invocation of CVC4 is done with a 10 minute timeout. To use a different timeout, set the `TEST_TIMEOUT` environment variable: @@ -35,10 +25,10 @@ To add a new regression file, add the file to git, for example: git add regress/regress0/testMyFunctionality.cvc ``` -Also add it to [Makefile.tests](Makefile.tests) in this directory. +Also add it to [CMakeLists.txt](CMakeLists.txt) in this directory. A number of regressions exist under test/regress that are not listed in -[Makefile.tests](Makefile.tests). These are regressions that may someday be +[CMakeLists.txt](CMakeLists.txt). These are regressions that may someday be included in the standard suite of tests, but are not yet included (perhaps they test functionality not yet supported). diff --git a/test/regress/regress0/bug217.smt2 b/test/regress/regress0/bug217.smt2 index 4d2e828b5..30c87333e 100644 --- a/test/regress/regress0/bug217.smt2 +++ b/test/regress/regress0/bug217.smt2 @@ -1,3 +1,4 @@ +; COMMAND-LINE: --fewer-preprocessing-holes ; EXPECT: unsat (set-logic QF_UF) (set-info :status unsat) diff --git a/test/regress/regress0/bv/ackermann3.smt2 b/test/regress/regress0/bv/ackermann3.smt2 new file mode 100644 index 000000000..8e47c8840 --- /dev/null +++ b/test/regress/regress0/bv/ackermann3.smt2 @@ -0,0 +1,23 @@ +; COMMAND-LINE: --bitblast=eager --no-check-models --no-check-proofs --no-check-unsat-cores +; EXPECT: unsat +(set-logic QF_ABV) +(set-info :smt-lib-version 2.0) +(set-info :category "crafted") +(set-info :status unsat) + +(define-sort bv () (_ BitVec 4)) +(define-sort abv () (Array bv bv)) + +(declare-fun v0 () (_ BitVec 4)) +(declare-fun v1 () (_ BitVec 4)) +(declare-fun a () abv) +(declare-fun b () abv) +(declare-fun c () abv) + +(assert (not (= (select a (select b (select c v0))) (select a (select b (select c v1)))))) + +(assert (= v0 v1)) + + +(check-sat) +(exit) diff --git a/test/regress/regress0/bv/ackermann4.smt2 b/test/regress/regress0/bv/ackermann4.smt2 new file mode 100644 index 000000000..cb8ad2e55 --- /dev/null +++ b/test/regress/regress0/bv/ackermann4.smt2 @@ -0,0 +1,16 @@ +; COMMAND-LINE: --bitblast=eager --no-check-models --no-check-proofs --no-check-unsat-cores +; EXPECT: sat +(set-logic QF_UFBV) +(set-info :smt-lib-version 2.0) +(set-info :category "crafted") +(set-info :status unsat) +(declare-fun v0 () (_ BitVec 4)) +(declare-fun f ((_ BitVec 4)) (_ BitVec 4)) +(declare-fun g ((_ BitVec 4)) (_ BitVec 4)) + +(assert (= (f v0) (g (f v0)))) +(assert (= (f (f v0)) (g (f v0)))) +(assert (= (f (f (f v0))) (g (f v0)))) + +(check-sat) +(exit) diff --git a/test/regress/regress0/bv/bool-to-bv.smt2 b/test/regress/regress0/bv/bool-to-bv.smt2 index 92c7e4117..8706c51a8 100644 --- a/test/regress/regress0/bv/bool-to-bv.smt2 +++ b/test/regress/regress0/bv/bool-to-bv.smt2 @@ -6,7 +6,14 @@ (declare-fun x0 () (_ BitVec 3)) (declare-fun b1 () Bool) (declare-fun b2 () Bool) +(declare-fun b3 () Bool) (assert (not (bvult (bvudiv (bvudiv (bvudiv x0 x0) x1) x2) x1))) +(assert (not (bvslt (bvudiv (bvudiv (bvudiv x0 x0) x1) x2) x1))) (assert (= #b000 x2)) (assert (=> b1 b2)) +(assert (and b1 b2)) +(assert (or b1 b2)) +(assert (xor b1 b3)) +(assert (not (xor b2 b2))) +(assert (ite b2 b2 b1)) (check-sat) diff --git a/test/regress/regress0/bv/bv-to-bool.smt b/test/regress/regress0/bv/bv-to-bool1.smt index ef4cec257..ef4cec257 100644 --- a/test/regress/regress0/bv/bv-to-bool.smt +++ b/test/regress/regress0/bv/bv-to-bool1.smt diff --git a/test/regress/regress0/bv/bv-to-bool2.smt2 b/test/regress/regress0/bv/bv-to-bool2.smt2 new file mode 100644 index 000000000..fb741733d --- /dev/null +++ b/test/regress/regress0/bv/bv-to-bool2.smt2 @@ -0,0 +1,11 @@ +; COMMAND-LINE: --bv-to-bool +; EXPECT: sat +(set-logic QF_BV) +(declare-fun v1 () (_ BitVec 1)) +(declare-fun v2 () (_ BitVec 1)) + +(assert (= (bvxor v2 v1) v1)) + + +(check-sat) +(exit) diff --git a/test/regress/regress0/quantifiers/macros-real-arg.smt2 b/test/regress/regress0/quantifiers/macros-real-arg.smt2 index edacdbe37..52eeedae6 100644 --- a/test/regress/regress0/quantifiers/macros-real-arg.smt2 +++ b/test/regress/regress0/quantifiers/macros-real-arg.smt2 @@ -3,7 +3,8 @@ ; this will fail if type rule for APPLY_UF is made strict (set-logic UFLIRA) (declare-fun P (Int) Bool) -(assert (forall ((x Int)) (P x))) +(declare-fun Q (Int) Bool) +(assert (and (forall ((x Int)) (P x)) (forall ((x Int)) (Q x)))) (declare-fun k () Real) (declare-fun k2 () Int) (assert (or (not (P (to_int k))) (not (P k2)))) diff --git a/test/regress/regress0/strings/unsound-repl-rewrite.smt2 b/test/regress/regress0/strings/unsound-repl-rewrite.smt2 new file mode 100644 index 000000000..02e4cc0b2 --- /dev/null +++ b/test/regress/regress0/strings/unsound-repl-rewrite.smt2 @@ -0,0 +1,8 @@ +; COMMAND-LINE: --strings-exp +; EXPECT: sat +(set-logic QF_S) +(declare-fun x () String) +(declare-fun y () String) +(declare-fun z () Int) +(assert (not (= (str.replace "B" (str.replace "" x "A") "B") (str.replace "B" x "B")))) +(check-sat) diff --git a/test/regress/regress1/sygus/commutative-stream.sy b/test/regress/regress1/sygus/commutative-stream.sy index 7b96a2bf3..8203fd9cf 100644 --- a/test/regress/regress1/sygus/commutative-stream.sy +++ b/test/regress/regress1/sygus/commutative-stream.sy @@ -3,7 +3,7 @@ ; EXPECT: (error "Maximum term size (2) for enumerative SyGuS exceeded.") ; EXIT: 1 -; COMMAND-LINE: --sygus-stream --sygus-abort-size=2 --decision=justification +; COMMAND-LINE: --sygus-stream --sygus-abort-size=2 --sygus-active-gen=none --decision=justification (set-logic LIA) diff --git a/test/unit/api/CMakeLists.txt b/test/unit/api/CMakeLists.txt index 90d34f7c6..eeab46f99 100644 --- a/test/unit/api/CMakeLists.txt +++ b/test/unit/api/CMakeLists.txt @@ -1,4 +1,6 @@ #-----------------------------------------------------------------------------# # Add unit tests -cvc4_add_unit_test_black(api_guards_black api) +cvc4_add_unit_test_black(solver_black api) +cvc4_add_unit_test_black(sort_black api) +cvc4_add_unit_test_black(term_black api) diff --git a/test/unit/api/api_guards_black.h b/test/unit/api/api_guards_black.h deleted file mode 100644 index 777ce81f1..000000000 --- a/test/unit/api/api_guards_black.h +++ /dev/null @@ -1,473 +0,0 @@ -/********************* */ -/*! \file api_guards_black.h - ** \verbatim - ** Top contributors (to current version): - ** Aina Niemetz - ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS - ** in the top-level source directory) and their institutional affiliations. - ** All rights reserved. See the file COPYING in the top-level source - ** directory for licensing information.\endverbatim - ** - ** \brief Black box testing of the guards of the C++ API functions. - ** - ** Black box testing of the guards of the C++ API functions. - **/ - -#include <cxxtest/TestSuite.h> - -#include "api/cvc4cpp.h" - -using namespace CVC4::api; - -class ApiGuardsBlack : public CxxTest::TestSuite -{ - public: - void setUp() override; - void tearDown() override; - - void testSolverMkBitVectorSort(); - void testSolverMkFloatingPointSort(); - void testSolverMkDatatypeSort(); - void testSolverMkFunctionSort(); - void testSolverMkPredicateSort(); - void testSolverMkTupleSort(); - void testSortGetDatatype(); - void testSortInstantiate(); - void testSortGetFunctionArity(); - void testSortGetFunctionDomainSorts(); - void testSortGetFunctionCodomainSort(); - void testSortGetArrayIndexSort(); - void testSortGetArrayElementSort(); - void testSortGetSetElementSort(); - void testSortGetUninterpretedSortName(); - void testSortIsUninterpretedSortParameterized(); - void testSortGetUninterpretedSortParamSorts(); - void testSortGetUninterpretedSortConstructorName(); - void testSortGetUninterpretedSortConstructorArity(); - void testSortGetBVSize(); - void testSortGetFPExponentSize(); - void testSortGetFPSignificandSize(); - void testSortGetDatatypeParamSorts(); - void testSortGetDatatypeArity(); - void testSortGetTupleLength(); - void testSortGetTupleSorts(); - void testSolverDeclareFun(); - void testSolverDefineFun(); - void testSolverDefineFunRec(); - void testSolverDefineFunsRec(); - - private: - Solver d_solver; -}; - -void ApiGuardsBlack::setUp() {} - -void ApiGuardsBlack::tearDown() {} - -void ApiGuardsBlack::testSolverMkBitVectorSort() -{ - TS_ASSERT_THROWS_NOTHING(d_solver.mkBitVectorSort(32)); - TS_ASSERT_THROWS(d_solver.mkBitVectorSort(0), CVC4ApiException&); -} - -void ApiGuardsBlack::testSolverMkFloatingPointSort() -{ - TS_ASSERT_THROWS_NOTHING(d_solver.mkFloatingPointSort(4, 8)); - TS_ASSERT_THROWS(d_solver.mkFloatingPointSort(0, 8), CVC4ApiException&); - TS_ASSERT_THROWS(d_solver.mkFloatingPointSort(4, 0), CVC4ApiException&); -} - -void ApiGuardsBlack::testSolverMkDatatypeSort() -{ - DatatypeDecl dtypeSpec("list"); - DatatypeConstructorDecl cons("cons"); - DatatypeSelectorDecl head("head", d_solver.getIntegerSort()); - cons.addSelector(head); - dtypeSpec.addConstructor(cons); - DatatypeConstructorDecl nil("nil"); - dtypeSpec.addConstructor(nil); - TS_ASSERT_THROWS_NOTHING(d_solver.mkDatatypeSort(dtypeSpec)); - DatatypeDecl throwsDtypeSpec("list"); - TS_ASSERT_THROWS(d_solver.mkDatatypeSort(throwsDtypeSpec), CVC4ApiException&); -} - -void ApiGuardsBlack::testSolverMkFunctionSort() -{ - TS_ASSERT_THROWS_NOTHING(d_solver.mkFunctionSort( - d_solver.mkUninterpretedSort("u"), d_solver.getIntegerSort())); - Sort funSort = d_solver.mkFunctionSort(d_solver.mkUninterpretedSort("u"), - d_solver.getIntegerSort()); - TS_ASSERT_THROWS(d_solver.mkFunctionSort(funSort, d_solver.getIntegerSort()), - CVC4ApiException&); - TS_ASSERT_THROWS(d_solver.mkFunctionSort(d_solver.getIntegerSort(), funSort), - CVC4ApiException&); - TS_ASSERT_THROWS_NOTHING(d_solver.mkFunctionSort( - {d_solver.mkUninterpretedSort("u"), d_solver.getIntegerSort()}, - d_solver.getIntegerSort())); - Sort funSort2 = d_solver.mkFunctionSort(d_solver.mkUninterpretedSort("u"), - d_solver.getIntegerSort()); - TS_ASSERT_THROWS( - d_solver.mkFunctionSort({funSort2, d_solver.mkUninterpretedSort("u")}, - d_solver.getIntegerSort()), - CVC4ApiException&); - TS_ASSERT_THROWS(d_solver.mkFunctionSort({d_solver.getIntegerSort(), - d_solver.mkUninterpretedSort("u")}, - funSort2), - CVC4ApiException&); -} - -void ApiGuardsBlack::testSolverMkPredicateSort() -{ - TS_ASSERT_THROWS_NOTHING( - d_solver.mkPredicateSort({d_solver.getIntegerSort()})); - TS_ASSERT_THROWS(d_solver.mkPredicateSort({}), CVC4ApiException&); - Sort funSort = d_solver.mkFunctionSort(d_solver.mkUninterpretedSort("u"), - d_solver.getIntegerSort()); - TS_ASSERT_THROWS( - d_solver.mkPredicateSort({d_solver.getIntegerSort(), funSort}), - CVC4ApiException&); -} - -void ApiGuardsBlack::testSolverMkTupleSort() -{ - TS_ASSERT_THROWS_NOTHING(d_solver.mkTupleSort({d_solver.getIntegerSort()})); - Sort funSort = d_solver.mkFunctionSort(d_solver.mkUninterpretedSort("u"), - d_solver.getIntegerSort()); - TS_ASSERT_THROWS(d_solver.mkTupleSort({d_solver.getIntegerSort(), funSort}), - CVC4ApiException&); -} - -void ApiGuardsBlack::testSortGetDatatype() -{ - // create datatype sort, check should not fail - DatatypeDecl dtypeSpec("list"); - DatatypeConstructorDecl cons("cons"); - DatatypeSelectorDecl head("head", d_solver.getIntegerSort()); - cons.addSelector(head); - dtypeSpec.addConstructor(cons); - DatatypeConstructorDecl nil("nil"); - dtypeSpec.addConstructor(nil); - Sort dtypeSort = d_solver.mkDatatypeSort(dtypeSpec); - TS_ASSERT_THROWS_NOTHING(dtypeSort.getDatatype()); - // create bv sort, check should fail - Sort bvSort = d_solver.mkBitVectorSort(32); - TS_ASSERT_THROWS(bvSort.getDatatype(), CVC4ApiException&); -} - -void ApiGuardsBlack::testSortInstantiate() -{ - // instantiate parametric datatype, check should not fail - Sort sort = d_solver.mkParamSort("T"); - DatatypeDecl paramDtypeSpec("paramlist", sort); - DatatypeConstructorDecl paramCons("cons"); - DatatypeConstructorDecl paramNil("nil"); - DatatypeSelectorDecl paramHead("head", sort); - paramCons.addSelector(paramHead); - paramDtypeSpec.addConstructor(paramCons); - paramDtypeSpec.addConstructor(paramNil); - Sort paramDtypeSort = d_solver.mkDatatypeSort(paramDtypeSpec); - TS_ASSERT_THROWS_NOTHING( - paramDtypeSort.instantiate(std::vector<Sort>{d_solver.getIntegerSort()})); - // instantiate non-parametric datatype sort, check should fail - DatatypeDecl dtypeSpec("list"); - DatatypeConstructorDecl cons("cons"); - DatatypeSelectorDecl head("head", d_solver.getIntegerSort()); - cons.addSelector(head); - dtypeSpec.addConstructor(cons); - DatatypeConstructorDecl nil("nil"); - dtypeSpec.addConstructor(nil); - Sort dtypeSort = d_solver.mkDatatypeSort(dtypeSpec); - TS_ASSERT_THROWS( - dtypeSort.instantiate(std::vector<Sort>{d_solver.getIntegerSort()}), - CVC4ApiException&); -} - -void ApiGuardsBlack::testSortGetFunctionArity() -{ - Sort funSort = d_solver.mkFunctionSort(d_solver.mkUninterpretedSort("u"), - d_solver.getIntegerSort()); - TS_ASSERT_THROWS_NOTHING(funSort.getFunctionArity()); - Sort bvSort = d_solver.mkBitVectorSort(32); - TS_ASSERT_THROWS(bvSort.getFunctionArity(), CVC4ApiException&); -} - -void ApiGuardsBlack::testSortGetFunctionDomainSorts() -{ - Sort funSort = d_solver.mkFunctionSort(d_solver.mkUninterpretedSort("u"), - d_solver.getIntegerSort()); - TS_ASSERT_THROWS_NOTHING(funSort.getFunctionDomainSorts()); - Sort bvSort = d_solver.mkBitVectorSort(32); - TS_ASSERT_THROWS(bvSort.getFunctionDomainSorts(), CVC4ApiException&); -} - -void ApiGuardsBlack::testSortGetFunctionCodomainSort() -{ - Sort funSort = d_solver.mkFunctionSort(d_solver.mkUninterpretedSort("u"), - d_solver.getIntegerSort()); - TS_ASSERT_THROWS_NOTHING(funSort.getFunctionCodomainSort()); - Sort bvSort = d_solver.mkBitVectorSort(32); - TS_ASSERT_THROWS(bvSort.getFunctionCodomainSort(), CVC4ApiException&); -} - -void ApiGuardsBlack::testSortGetArrayIndexSort() -{ - Sort elementSort = d_solver.mkBitVectorSort(32); - Sort indexSort = d_solver.mkBitVectorSort(32); - Sort arraySort = d_solver.mkArraySort(indexSort, elementSort); - TS_ASSERT_THROWS_NOTHING(arraySort.getArrayIndexSort()); - TS_ASSERT_THROWS(indexSort.getArrayIndexSort(), CVC4ApiException&); -} - -void ApiGuardsBlack::testSortGetArrayElementSort() -{ - Sort elementSort = d_solver.mkBitVectorSort(32); - Sort indexSort = d_solver.mkBitVectorSort(32); - Sort arraySort = d_solver.mkArraySort(indexSort, elementSort); - TS_ASSERT_THROWS_NOTHING(arraySort.getArrayElementSort()); - TS_ASSERT_THROWS(indexSort.getArrayElementSort(), CVC4ApiException&); -} - -void ApiGuardsBlack::testSortGetSetElementSort() -{ - Sort setSort = d_solver.mkSetSort(d_solver.getIntegerSort()); - TS_ASSERT_THROWS_NOTHING(setSort.getSetElementSort()); - Sort bvSort = d_solver.mkBitVectorSort(32); - TS_ASSERT_THROWS(bvSort.getSetElementSort(), CVC4ApiException&); -} - -void ApiGuardsBlack::testSortGetUninterpretedSortName() -{ - Sort uSort = d_solver.mkUninterpretedSort("u"); - TS_ASSERT_THROWS_NOTHING(uSort.getUninterpretedSortName()); - Sort bvSort = d_solver.mkBitVectorSort(32); - TS_ASSERT_THROWS(bvSort.getUninterpretedSortName(), CVC4ApiException&); -} - -void ApiGuardsBlack::testSortIsUninterpretedSortParameterized() -{ - Sort uSort = d_solver.mkUninterpretedSort("u"); - TS_ASSERT_THROWS_NOTHING(uSort.isUninterpretedSortParameterized()); - Sort bvSort = d_solver.mkBitVectorSort(32); - TS_ASSERT_THROWS(bvSort.isUninterpretedSortParameterized(), - CVC4ApiException&); -} - -void ApiGuardsBlack::testSortGetUninterpretedSortParamSorts() -{ - Sort uSort = d_solver.mkUninterpretedSort("u"); - TS_ASSERT_THROWS_NOTHING(uSort.getUninterpretedSortParamSorts()); - Sort bvSort = d_solver.mkBitVectorSort(32); - TS_ASSERT_THROWS(bvSort.getUninterpretedSortParamSorts(), CVC4ApiException&); -} - -void ApiGuardsBlack::testSortGetUninterpretedSortConstructorName() -{ - Sort sSort = d_solver.mkSortConstructorSort("s", 2); - TS_ASSERT_THROWS_NOTHING(sSort.getSortConstructorName()); - Sort bvSort = d_solver.mkBitVectorSort(32); - TS_ASSERT_THROWS(bvSort.getSortConstructorName(), CVC4ApiException&); -} - -void ApiGuardsBlack::testSortGetUninterpretedSortConstructorArity() -{ - Sort sSort = d_solver.mkSortConstructorSort("s", 2); - TS_ASSERT_THROWS_NOTHING(sSort.getSortConstructorArity()); - Sort bvSort = d_solver.mkBitVectorSort(32); - TS_ASSERT_THROWS(bvSort.getSortConstructorArity(), CVC4ApiException&); -} - -void ApiGuardsBlack::testSortGetBVSize() -{ - Sort bvSort = d_solver.mkBitVectorSort(32); - TS_ASSERT_THROWS_NOTHING(bvSort.getBVSize()); - Sort setSort = d_solver.mkSetSort(d_solver.getIntegerSort()); - TS_ASSERT_THROWS(setSort.getBVSize(), CVC4ApiException&); -} - -void ApiGuardsBlack::testSortGetFPExponentSize() -{ - Sort fpSort = d_solver.mkFloatingPointSort(4, 8); - TS_ASSERT_THROWS_NOTHING(fpSort.getFPExponentSize()); - Sort setSort = d_solver.mkSetSort(d_solver.getIntegerSort()); - TS_ASSERT_THROWS(setSort.getFPExponentSize(), CVC4ApiException&); -} - -void ApiGuardsBlack::testSortGetFPSignificandSize() -{ - Sort fpSort = d_solver.mkFloatingPointSort(4, 8); - TS_ASSERT_THROWS_NOTHING(fpSort.getFPSignificandSize()); - Sort setSort = d_solver.mkSetSort(d_solver.getIntegerSort()); - TS_ASSERT_THROWS(setSort.getFPSignificandSize(), CVC4ApiException&); -} - -void ApiGuardsBlack::testSortGetDatatypeParamSorts() -{ - // create parametric datatype, check should not fail - Sort sort = d_solver.mkParamSort("T"); - DatatypeDecl paramDtypeSpec("paramlist", sort); - DatatypeConstructorDecl paramCons("cons"); - DatatypeConstructorDecl paramNil("nil"); - DatatypeSelectorDecl paramHead("head", sort); - paramCons.addSelector(paramHead); - paramDtypeSpec.addConstructor(paramCons); - paramDtypeSpec.addConstructor(paramNil); - Sort paramDtypeSort = d_solver.mkDatatypeSort(paramDtypeSpec); - TS_ASSERT_THROWS_NOTHING(paramDtypeSort.getDatatypeParamSorts()); - // create non-parametric datatype sort, check should fail - DatatypeDecl dtypeSpec("list"); - DatatypeConstructorDecl cons("cons"); - DatatypeSelectorDecl head("head", d_solver.getIntegerSort()); - cons.addSelector(head); - dtypeSpec.addConstructor(cons); - DatatypeConstructorDecl nil("nil"); - dtypeSpec.addConstructor(nil); - Sort dtypeSort = d_solver.mkDatatypeSort(dtypeSpec); - TS_ASSERT_THROWS(dtypeSort.getDatatypeParamSorts(), CVC4ApiException&); -} - -void ApiGuardsBlack::testSortGetDatatypeArity() -{ - // create datatype sort, check should not fail - DatatypeDecl dtypeSpec("list"); - DatatypeConstructorDecl cons("cons"); - DatatypeSelectorDecl head("head", d_solver.getIntegerSort()); - cons.addSelector(head); - dtypeSpec.addConstructor(cons); - DatatypeConstructorDecl nil("nil"); - dtypeSpec.addConstructor(nil); - Sort dtypeSort = d_solver.mkDatatypeSort(dtypeSpec); - TS_ASSERT_THROWS_NOTHING(dtypeSort.getDatatypeArity()); - // create bv sort, check should fail - Sort bvSort = d_solver.mkBitVectorSort(32); - TS_ASSERT_THROWS(bvSort.getDatatypeArity(), CVC4ApiException&); -} - -void ApiGuardsBlack::testSortGetTupleLength() -{ - Sort tupleSort = d_solver.mkTupleSort( - {d_solver.getIntegerSort(), d_solver.getIntegerSort()}); - TS_ASSERT_THROWS_NOTHING(tupleSort.getTupleLength()); - Sort bvSort = d_solver.mkBitVectorSort(32); - TS_ASSERT_THROWS(bvSort.getTupleLength(), CVC4ApiException&); -} - -void ApiGuardsBlack::testSortGetTupleSorts() -{ - Sort tupleSort = d_solver.mkTupleSort( - {d_solver.getIntegerSort(), d_solver.getIntegerSort()}); - TS_ASSERT_THROWS_NOTHING(tupleSort.getTupleSorts()); - Sort bvSort = d_solver.mkBitVectorSort(32); - TS_ASSERT_THROWS(bvSort.getTupleSorts(), CVC4ApiException&); -} - -void ApiGuardsBlack::testSolverDeclareFun() -{ - Sort bvSort = d_solver.mkBitVectorSort(32); - Sort funSort = d_solver.mkFunctionSort(d_solver.mkUninterpretedSort("u"), - d_solver.getIntegerSort()); - TS_ASSERT_THROWS_NOTHING(d_solver.declareFun("f1", bvSort)); - TS_ASSERT_THROWS_NOTHING(d_solver.declareFun("f2", funSort)); - TS_ASSERT_THROWS_NOTHING( - d_solver.declareFun("f3", {bvSort, d_solver.getIntegerSort()}, bvSort)); - TS_ASSERT_THROWS(d_solver.declareFun("f4", {bvSort, funSort}, bvSort), - CVC4ApiException&); - TS_ASSERT_THROWS(d_solver.declareFun("f5", {bvSort, bvSort}, funSort), - CVC4ApiException&); -} - -void ApiGuardsBlack::testSolverDefineFun() -{ - Sort bvSort = d_solver.mkBitVectorSort(32); - Sort funSort1 = d_solver.mkFunctionSort({bvSort, bvSort}, bvSort); - Sort funSort2 = d_solver.mkFunctionSort(d_solver.mkUninterpretedSort("u"), - d_solver.getIntegerSort()); - Term b1 = d_solver.mkBoundVar("b1", bvSort); - Term b11 = d_solver.mkBoundVar("b1", bvSort); - Term b2 = d_solver.mkBoundVar("b2", d_solver.getIntegerSort()); - Term b3 = d_solver.mkBoundVar("b3", funSort2); - Term v1 = d_solver.mkBoundVar("v1", bvSort); - Term v2 = d_solver.mkBoundVar("v2", d_solver.getIntegerSort()); - Term v3 = d_solver.mkVar("v3", funSort2); - Term f1 = d_solver.declareFun("f1", funSort1); - Term f2 = d_solver.declareFun("f2", funSort2); - Term f3 = d_solver.declareFun("f3", bvSort); - TS_ASSERT_THROWS_NOTHING(d_solver.defineFun("f", {}, bvSort, v1)); - TS_ASSERT_THROWS_NOTHING(d_solver.defineFun("ff", {b1, b2}, bvSort, v1)); - TS_ASSERT_THROWS_NOTHING(d_solver.defineFun(f1, {b1, b11}, v1)); - TS_ASSERT_THROWS(d_solver.defineFun("fff", {b1}, bvSort, v3), - CVC4ApiException&); - TS_ASSERT_THROWS(d_solver.defineFun("ffff", {b1}, funSort2, v3), - CVC4ApiException&); - TS_ASSERT_THROWS(d_solver.defineFun("fffff", {b1, b3}, bvSort, v1), - CVC4ApiException&); - TS_ASSERT_THROWS(d_solver.defineFun(f1, {b1}, v1), CVC4ApiException&); - TS_ASSERT_THROWS(d_solver.defineFun(f1, {b1, b11}, v2), CVC4ApiException&); - TS_ASSERT_THROWS(d_solver.defineFun(f1, {b1, b11}, v3), CVC4ApiException&); - TS_ASSERT_THROWS(d_solver.defineFun(f2, {b1}, v2), CVC4ApiException&); - TS_ASSERT_THROWS(d_solver.defineFun(f3, {b1}, v1), CVC4ApiException&); -} - -void ApiGuardsBlack::testSolverDefineFunRec() -{ - Sort bvSort = d_solver.mkBitVectorSort(32); - Sort funSort1 = d_solver.mkFunctionSort({bvSort, bvSort}, bvSort); - Sort funSort2 = d_solver.mkFunctionSort(d_solver.mkUninterpretedSort("u"), - d_solver.getIntegerSort()); - Term b1 = d_solver.mkBoundVar("b1", bvSort); - Term b11 = d_solver.mkBoundVar("b1", bvSort); - Term b2 = d_solver.mkBoundVar("b2", d_solver.getIntegerSort()); - Term b3 = d_solver.mkBoundVar("b3", funSort2); - Term v1 = d_solver.mkBoundVar("v1", bvSort); - Term v2 = d_solver.mkBoundVar("v2", d_solver.getIntegerSort()); - Term v3 = d_solver.mkVar("v3", funSort2); - Term f1 = d_solver.declareFun("f1", funSort1); - Term f2 = d_solver.declareFun("f2", funSort2); - Term f3 = d_solver.declareFun("f3", bvSort); - TS_ASSERT_THROWS_NOTHING(d_solver.defineFunRec("f", {}, bvSort, v1)); - TS_ASSERT_THROWS_NOTHING(d_solver.defineFunRec("ff", {b1, b2}, bvSort, v1)); - TS_ASSERT_THROWS_NOTHING(d_solver.defineFunRec(f1, {b1, b11}, v1)); - TS_ASSERT_THROWS(d_solver.defineFunRec("fff", {b1}, bvSort, v3), - CVC4ApiException&); - TS_ASSERT_THROWS(d_solver.defineFunRec("ffff", {b1}, funSort2, v3), - CVC4ApiException&); - TS_ASSERT_THROWS(d_solver.defineFunRec("fffff", {b1, b3}, bvSort, v1), - CVC4ApiException&); - TS_ASSERT_THROWS(d_solver.defineFunRec(f1, {b1}, v1), CVC4ApiException&); - TS_ASSERT_THROWS(d_solver.defineFunRec(f1, {b1, b11}, v2), CVC4ApiException&); - TS_ASSERT_THROWS(d_solver.defineFunRec(f1, {b1, b11}, v3), CVC4ApiException&); - TS_ASSERT_THROWS(d_solver.defineFunRec(f2, {b1}, v2), CVC4ApiException&); - TS_ASSERT_THROWS(d_solver.defineFunRec(f3, {b1}, v1), CVC4ApiException&); -} - -void ApiGuardsBlack::testSolverDefineFunsRec() -{ - Sort uSort = d_solver.mkUninterpretedSort("u"); - Sort bvSort = d_solver.mkBitVectorSort(32); - Sort funSort1 = d_solver.mkFunctionSort({bvSort, bvSort}, bvSort); - Sort funSort2 = d_solver.mkFunctionSort(uSort, d_solver.getIntegerSort()); - Term b1 = d_solver.mkBoundVar("b1", bvSort); - Term b11 = d_solver.mkBoundVar("b1", bvSort); - Term b2 = d_solver.mkBoundVar("b2", d_solver.getIntegerSort()); - Term b3 = d_solver.mkBoundVar("b3", funSort2); - Term b4 = d_solver.mkBoundVar("b4", uSort); - Term v1 = d_solver.mkBoundVar("v1", bvSort); - Term v2 = d_solver.mkBoundVar("v2", d_solver.getIntegerSort()); - Term v3 = d_solver.mkVar("v3", funSort2); - Term v4 = d_solver.mkVar("v4", uSort); - Term f1 = d_solver.declareFun("f1", funSort1); - Term f2 = d_solver.declareFun("f2", funSort2); - Term f3 = d_solver.declareFun("f3", bvSort); - TS_ASSERT_THROWS_NOTHING( - d_solver.defineFunsRec({f1, f2}, {{b1, b11}, {b4}}, {v1, v2})); - TS_ASSERT_THROWS( - d_solver.defineFunsRec({f1, f3}, {{b1, b11}, {b4}}, {v1, v2}), - CVC4ApiException&); - TS_ASSERT_THROWS(d_solver.defineFunsRec({f1, f2}, {{b1}, {b4}}, {v1, v2}), - CVC4ApiException&); - TS_ASSERT_THROWS(d_solver.defineFunsRec({f1, f2}, {{b1, b2}, {b4}}, {v1, v2}), - CVC4ApiException&); - TS_ASSERT_THROWS( - d_solver.defineFunsRec({f1, f2}, {{b1, b11}, {b4}}, {v1, v4}), - CVC4ApiException&); -} diff --git a/test/unit/api/solver_black.h b/test/unit/api/solver_black.h new file mode 100644 index 000000000..538899a0f --- /dev/null +++ b/test/unit/api/solver_black.h @@ -0,0 +1,230 @@ +/********************* */ +/*! \file api_guards_black.h + ** \verbatim + ** Top contributors (to current version): + ** Aina Niemetz + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS + ** in the top-level source directory) and their institutional affiliations. + ** All rights reserved. See the file COPYING in the top-level source + ** directory for licensing information.\endverbatim + ** + ** \brief Black box testing of the guards of the C++ API functions. + ** + ** Black box testing of the guards of the C++ API functions. + **/ + +#include <cxxtest/TestSuite.h> + +#include "api/cvc4cpp.h" + +using namespace CVC4::api; + +class SolverBlack : public CxxTest::TestSuite +{ + public: + void setUp() override; + void tearDown() override; + + void testMkBitVectorSort(); + void testMkFloatingPointSort(); + void testMkDatatypeSort(); + void testMkFunctionSort(); + void testMkPredicateSort(); + void testMkTupleSort(); + void testDeclareFun(); + void testDefineFun(); + void testDefineFunRec(); + void testDefineFunsRec(); + + private: + Solver d_solver; +}; + +void SolverBlack::setUp() {} + +void SolverBlack::tearDown() {} + +void SolverBlack::testMkBitVectorSort() +{ + TS_ASSERT_THROWS_NOTHING(d_solver.mkBitVectorSort(32)); + TS_ASSERT_THROWS(d_solver.mkBitVectorSort(0), CVC4ApiException&); +} + +void SolverBlack::testMkFloatingPointSort() +{ + TS_ASSERT_THROWS_NOTHING(d_solver.mkFloatingPointSort(4, 8)); + TS_ASSERT_THROWS(d_solver.mkFloatingPointSort(0, 8), CVC4ApiException&); + TS_ASSERT_THROWS(d_solver.mkFloatingPointSort(4, 0), CVC4ApiException&); +} + +void SolverBlack::testMkDatatypeSort() +{ + DatatypeDecl dtypeSpec("list"); + DatatypeConstructorDecl cons("cons"); + DatatypeSelectorDecl head("head", d_solver.getIntegerSort()); + cons.addSelector(head); + dtypeSpec.addConstructor(cons); + DatatypeConstructorDecl nil("nil"); + dtypeSpec.addConstructor(nil); + TS_ASSERT_THROWS_NOTHING(d_solver.mkDatatypeSort(dtypeSpec)); + DatatypeDecl throwsDtypeSpec("list"); + TS_ASSERT_THROWS(d_solver.mkDatatypeSort(throwsDtypeSpec), CVC4ApiException&); +} + +void SolverBlack::testMkFunctionSort() +{ + TS_ASSERT_THROWS_NOTHING(d_solver.mkFunctionSort( + d_solver.mkUninterpretedSort("u"), d_solver.getIntegerSort())); + Sort funSort = d_solver.mkFunctionSort(d_solver.mkUninterpretedSort("u"), + d_solver.getIntegerSort()); + TS_ASSERT_THROWS(d_solver.mkFunctionSort(funSort, d_solver.getIntegerSort()), + CVC4ApiException&); + TS_ASSERT_THROWS(d_solver.mkFunctionSort(d_solver.getIntegerSort(), funSort), + CVC4ApiException&); + TS_ASSERT_THROWS_NOTHING(d_solver.mkFunctionSort( + {d_solver.mkUninterpretedSort("u"), d_solver.getIntegerSort()}, + d_solver.getIntegerSort())); + Sort funSort2 = d_solver.mkFunctionSort(d_solver.mkUninterpretedSort("u"), + d_solver.getIntegerSort()); + TS_ASSERT_THROWS( + d_solver.mkFunctionSort({funSort2, d_solver.mkUninterpretedSort("u")}, + d_solver.getIntegerSort()), + CVC4ApiException&); + TS_ASSERT_THROWS(d_solver.mkFunctionSort({d_solver.getIntegerSort(), + d_solver.mkUninterpretedSort("u")}, + funSort2), + CVC4ApiException&); +} + +void SolverBlack::testMkPredicateSort() +{ + TS_ASSERT_THROWS_NOTHING( + d_solver.mkPredicateSort({d_solver.getIntegerSort()})); + TS_ASSERT_THROWS(d_solver.mkPredicateSort({}), CVC4ApiException&); + Sort funSort = d_solver.mkFunctionSort(d_solver.mkUninterpretedSort("u"), + d_solver.getIntegerSort()); + TS_ASSERT_THROWS( + d_solver.mkPredicateSort({d_solver.getIntegerSort(), funSort}), + CVC4ApiException&); +} + +void SolverBlack::testMkTupleSort() +{ + TS_ASSERT_THROWS_NOTHING(d_solver.mkTupleSort({d_solver.getIntegerSort()})); + Sort funSort = d_solver.mkFunctionSort(d_solver.mkUninterpretedSort("u"), + d_solver.getIntegerSort()); + TS_ASSERT_THROWS(d_solver.mkTupleSort({d_solver.getIntegerSort(), funSort}), + CVC4ApiException&); +} + +void SolverBlack::testDeclareFun() +{ + Sort bvSort = d_solver.mkBitVectorSort(32); + Sort funSort = d_solver.mkFunctionSort(d_solver.mkUninterpretedSort("u"), + d_solver.getIntegerSort()); + TS_ASSERT_THROWS_NOTHING(d_solver.declareFun("f1", bvSort)); + TS_ASSERT_THROWS_NOTHING(d_solver.declareFun("f2", funSort)); + TS_ASSERT_THROWS_NOTHING( + d_solver.declareFun("f3", {bvSort, d_solver.getIntegerSort()}, bvSort)); + TS_ASSERT_THROWS(d_solver.declareFun("f4", {bvSort, funSort}, bvSort), + CVC4ApiException&); + TS_ASSERT_THROWS(d_solver.declareFun("f5", {bvSort, bvSort}, funSort), + CVC4ApiException&); +} + +void SolverBlack::testDefineFun() +{ + Sort bvSort = d_solver.mkBitVectorSort(32); + Sort funSort1 = d_solver.mkFunctionSort({bvSort, bvSort}, bvSort); + Sort funSort2 = d_solver.mkFunctionSort(d_solver.mkUninterpretedSort("u"), + d_solver.getIntegerSort()); + Term b1 = d_solver.mkBoundVar("b1", bvSort); + Term b11 = d_solver.mkBoundVar("b1", bvSort); + Term b2 = d_solver.mkBoundVar("b2", d_solver.getIntegerSort()); + Term b3 = d_solver.mkBoundVar("b3", funSort2); + Term v1 = d_solver.mkBoundVar("v1", bvSort); + Term v2 = d_solver.mkBoundVar("v2", d_solver.getIntegerSort()); + Term v3 = d_solver.mkVar("v3", funSort2); + Term f1 = d_solver.declareFun("f1", funSort1); + Term f2 = d_solver.declareFun("f2", funSort2); + Term f3 = d_solver.declareFun("f3", bvSort); + TS_ASSERT_THROWS_NOTHING(d_solver.defineFun("f", {}, bvSort, v1)); + TS_ASSERT_THROWS_NOTHING(d_solver.defineFun("ff", {b1, b2}, bvSort, v1)); + TS_ASSERT_THROWS_NOTHING(d_solver.defineFun(f1, {b1, b11}, v1)); + TS_ASSERT_THROWS(d_solver.defineFun("fff", {b1}, bvSort, v3), + CVC4ApiException&); + TS_ASSERT_THROWS(d_solver.defineFun("ffff", {b1}, funSort2, v3), + CVC4ApiException&); + TS_ASSERT_THROWS(d_solver.defineFun("fffff", {b1, b3}, bvSort, v1), + CVC4ApiException&); + TS_ASSERT_THROWS(d_solver.defineFun(f1, {b1}, v1), CVC4ApiException&); + TS_ASSERT_THROWS(d_solver.defineFun(f1, {b1, b11}, v2), CVC4ApiException&); + TS_ASSERT_THROWS(d_solver.defineFun(f1, {b1, b11}, v3), CVC4ApiException&); + TS_ASSERT_THROWS(d_solver.defineFun(f2, {b1}, v2), CVC4ApiException&); + TS_ASSERT_THROWS(d_solver.defineFun(f3, {b1}, v1), CVC4ApiException&); +} + +void SolverBlack::testDefineFunRec() +{ + Sort bvSort = d_solver.mkBitVectorSort(32); + Sort funSort1 = d_solver.mkFunctionSort({bvSort, bvSort}, bvSort); + Sort funSort2 = d_solver.mkFunctionSort(d_solver.mkUninterpretedSort("u"), + d_solver.getIntegerSort()); + Term b1 = d_solver.mkBoundVar("b1", bvSort); + Term b11 = d_solver.mkBoundVar("b1", bvSort); + Term b2 = d_solver.mkBoundVar("b2", d_solver.getIntegerSort()); + Term b3 = d_solver.mkBoundVar("b3", funSort2); + Term v1 = d_solver.mkBoundVar("v1", bvSort); + Term v2 = d_solver.mkBoundVar("v2", d_solver.getIntegerSort()); + Term v3 = d_solver.mkVar("v3", funSort2); + Term f1 = d_solver.declareFun("f1", funSort1); + Term f2 = d_solver.declareFun("f2", funSort2); + Term f3 = d_solver.declareFun("f3", bvSort); + TS_ASSERT_THROWS_NOTHING(d_solver.defineFunRec("f", {}, bvSort, v1)); + TS_ASSERT_THROWS_NOTHING(d_solver.defineFunRec("ff", {b1, b2}, bvSort, v1)); + TS_ASSERT_THROWS_NOTHING(d_solver.defineFunRec(f1, {b1, b11}, v1)); + TS_ASSERT_THROWS(d_solver.defineFunRec("fff", {b1}, bvSort, v3), + CVC4ApiException&); + TS_ASSERT_THROWS(d_solver.defineFunRec("ffff", {b1}, funSort2, v3), + CVC4ApiException&); + TS_ASSERT_THROWS(d_solver.defineFunRec("fffff", {b1, b3}, bvSort, v1), + CVC4ApiException&); + TS_ASSERT_THROWS(d_solver.defineFunRec(f1, {b1}, v1), CVC4ApiException&); + TS_ASSERT_THROWS(d_solver.defineFunRec(f1, {b1, b11}, v2), CVC4ApiException&); + TS_ASSERT_THROWS(d_solver.defineFunRec(f1, {b1, b11}, v3), CVC4ApiException&); + TS_ASSERT_THROWS(d_solver.defineFunRec(f2, {b1}, v2), CVC4ApiException&); + TS_ASSERT_THROWS(d_solver.defineFunRec(f3, {b1}, v1), CVC4ApiException&); +} + +void SolverBlack::testDefineFunsRec() +{ + Sort uSort = d_solver.mkUninterpretedSort("u"); + Sort bvSort = d_solver.mkBitVectorSort(32); + Sort funSort1 = d_solver.mkFunctionSort({bvSort, bvSort}, bvSort); + Sort funSort2 = d_solver.mkFunctionSort(uSort, d_solver.getIntegerSort()); + Term b1 = d_solver.mkBoundVar("b1", bvSort); + Term b11 = d_solver.mkBoundVar("b1", bvSort); + Term b2 = d_solver.mkBoundVar("b2", d_solver.getIntegerSort()); + Term b3 = d_solver.mkBoundVar("b3", funSort2); + Term b4 = d_solver.mkBoundVar("b4", uSort); + Term v1 = d_solver.mkBoundVar("v1", bvSort); + Term v2 = d_solver.mkBoundVar("v2", d_solver.getIntegerSort()); + Term v3 = d_solver.mkVar("v3", funSort2); + Term v4 = d_solver.mkVar("v4", uSort); + Term f1 = d_solver.declareFun("f1", funSort1); + Term f2 = d_solver.declareFun("f2", funSort2); + Term f3 = d_solver.declareFun("f3", bvSort); + TS_ASSERT_THROWS_NOTHING( + d_solver.defineFunsRec({f1, f2}, {{b1, b11}, {b4}}, {v1, v2})); + TS_ASSERT_THROWS( + d_solver.defineFunsRec({f1, f3}, {{b1, b11}, {b4}}, {v1, v2}), + CVC4ApiException&); + TS_ASSERT_THROWS(d_solver.defineFunsRec({f1, f2}, {{b1}, {b4}}, {v1, v2}), + CVC4ApiException&); + TS_ASSERT_THROWS(d_solver.defineFunsRec({f1, f2}, {{b1, b2}, {b4}}, {v1, v2}), + CVC4ApiException&); + TS_ASSERT_THROWS( + d_solver.defineFunsRec({f1, f2}, {{b1, b11}, {b4}}, {v1, v4}), + CVC4ApiException&); +} diff --git a/test/unit/api/sort_black.h b/test/unit/api/sort_black.h new file mode 100644 index 000000000..d9337e627 --- /dev/null +++ b/test/unit/api/sort_black.h @@ -0,0 +1,279 @@ +/********************* */ +/*! \file api_guards_black.h + ** \verbatim + ** Top contributors (to current version): + ** Aina Niemetz + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS + ** in the top-level source directory) and their institutional affiliations. + ** All rights reserved. See the file COPYING in the top-level source + ** directory for licensing information.\endverbatim + ** + ** \brief Black box testing of the guards of the C++ API functions. + ** + ** Black box testing of the guards of the C++ API functions. + **/ + +#include <cxxtest/TestSuite.h> + +#include "api/cvc4cpp.h" + +using namespace CVC4::api; + +class SortBlack : public CxxTest::TestSuite +{ + public: + void setUp() override; + void tearDown() override; + + void testGetDatatype(); + void testInstantiate(); + void testGetFunctionArity(); + void testGetFunctionDomainSorts(); + void testGetFunctionCodomainSort(); + void testGetArrayIndexSort(); + void testGetArrayElementSort(); + void testGetSetElementSort(); + void testGetUninterpretedSortName(); + void testIsUninterpretedSortParameterized(); + void testGetUninterpretedSortParamSorts(); + void testGetUninterpretedSortConstructorName(); + void testGetUninterpretedSortConstructorArity(); + void testGetBVSize(); + void testGetFPExponentSize(); + void testGetFPSignificandSize(); + void testGetDatatypeParamSorts(); + void testGetDatatypeArity(); + void testGetTupleLength(); + void testGetTupleSorts(); + + private: + Solver d_solver; +}; + +void SortBlack::setUp() {} + +void SortBlack::tearDown() {} + +void SortBlack::testGetDatatype() +{ + // create datatype sort, check should not fail + DatatypeDecl dtypeSpec("list"); + DatatypeConstructorDecl cons("cons"); + DatatypeSelectorDecl head("head", d_solver.getIntegerSort()); + cons.addSelector(head); + dtypeSpec.addConstructor(cons); + DatatypeConstructorDecl nil("nil"); + dtypeSpec.addConstructor(nil); + Sort dtypeSort = d_solver.mkDatatypeSort(dtypeSpec); + TS_ASSERT_THROWS_NOTHING(dtypeSort.getDatatype()); + // create bv sort, check should fail + Sort bvSort = d_solver.mkBitVectorSort(32); + TS_ASSERT_THROWS(bvSort.getDatatype(), CVC4ApiException&); +} + +void SortBlack::testInstantiate() +{ + // instantiate parametric datatype, check should not fail + Sort sort = d_solver.mkParamSort("T"); + DatatypeDecl paramDtypeSpec("paramlist", sort); + DatatypeConstructorDecl paramCons("cons"); + DatatypeConstructorDecl paramNil("nil"); + DatatypeSelectorDecl paramHead("head", sort); + paramCons.addSelector(paramHead); + paramDtypeSpec.addConstructor(paramCons); + paramDtypeSpec.addConstructor(paramNil); + Sort paramDtypeSort = d_solver.mkDatatypeSort(paramDtypeSpec); + TS_ASSERT_THROWS_NOTHING( + paramDtypeSort.instantiate(std::vector<Sort>{d_solver.getIntegerSort()})); + // instantiate non-parametric datatype sort, check should fail + DatatypeDecl dtypeSpec("list"); + DatatypeConstructorDecl cons("cons"); + DatatypeSelectorDecl head("head", d_solver.getIntegerSort()); + cons.addSelector(head); + dtypeSpec.addConstructor(cons); + DatatypeConstructorDecl nil("nil"); + dtypeSpec.addConstructor(nil); + Sort dtypeSort = d_solver.mkDatatypeSort(dtypeSpec); + TS_ASSERT_THROWS( + dtypeSort.instantiate(std::vector<Sort>{d_solver.getIntegerSort()}), + CVC4ApiException&); +} + +void SortBlack::testGetFunctionArity() +{ + Sort funSort = d_solver.mkFunctionSort(d_solver.mkUninterpretedSort("u"), + d_solver.getIntegerSort()); + TS_ASSERT_THROWS_NOTHING(funSort.getFunctionArity()); + Sort bvSort = d_solver.mkBitVectorSort(32); + TS_ASSERT_THROWS(bvSort.getFunctionArity(), CVC4ApiException&); +} + +void SortBlack::testGetFunctionDomainSorts() +{ + Sort funSort = d_solver.mkFunctionSort(d_solver.mkUninterpretedSort("u"), + d_solver.getIntegerSort()); + TS_ASSERT_THROWS_NOTHING(funSort.getFunctionDomainSorts()); + Sort bvSort = d_solver.mkBitVectorSort(32); + TS_ASSERT_THROWS(bvSort.getFunctionDomainSorts(), CVC4ApiException&); +} + +void SortBlack::testGetFunctionCodomainSort() +{ + Sort funSort = d_solver.mkFunctionSort(d_solver.mkUninterpretedSort("u"), + d_solver.getIntegerSort()); + TS_ASSERT_THROWS_NOTHING(funSort.getFunctionCodomainSort()); + Sort bvSort = d_solver.mkBitVectorSort(32); + TS_ASSERT_THROWS(bvSort.getFunctionCodomainSort(), CVC4ApiException&); +} + +void SortBlack::testGetArrayIndexSort() +{ + Sort elementSort = d_solver.mkBitVectorSort(32); + Sort indexSort = d_solver.mkBitVectorSort(32); + Sort arraySort = d_solver.mkArraySort(indexSort, elementSort); + TS_ASSERT_THROWS_NOTHING(arraySort.getArrayIndexSort()); + TS_ASSERT_THROWS(indexSort.getArrayIndexSort(), CVC4ApiException&); +} + +void SortBlack::testGetArrayElementSort() +{ + Sort elementSort = d_solver.mkBitVectorSort(32); + Sort indexSort = d_solver.mkBitVectorSort(32); + Sort arraySort = d_solver.mkArraySort(indexSort, elementSort); + TS_ASSERT_THROWS_NOTHING(arraySort.getArrayElementSort()); + TS_ASSERT_THROWS(indexSort.getArrayElementSort(), CVC4ApiException&); +} + +void SortBlack::testGetSetElementSort() +{ + Sort setSort = d_solver.mkSetSort(d_solver.getIntegerSort()); + TS_ASSERT_THROWS_NOTHING(setSort.getSetElementSort()); + Sort bvSort = d_solver.mkBitVectorSort(32); + TS_ASSERT_THROWS(bvSort.getSetElementSort(), CVC4ApiException&); +} + +void SortBlack::testGetUninterpretedSortName() +{ + Sort uSort = d_solver.mkUninterpretedSort("u"); + TS_ASSERT_THROWS_NOTHING(uSort.getUninterpretedSortName()); + Sort bvSort = d_solver.mkBitVectorSort(32); + TS_ASSERT_THROWS(bvSort.getUninterpretedSortName(), CVC4ApiException&); +} + +void SortBlack::testIsUninterpretedSortParameterized() +{ + Sort uSort = d_solver.mkUninterpretedSort("u"); + TS_ASSERT_THROWS_NOTHING(uSort.isUninterpretedSortParameterized()); + Sort bvSort = d_solver.mkBitVectorSort(32); + TS_ASSERT_THROWS(bvSort.isUninterpretedSortParameterized(), + CVC4ApiException&); +} + +void SortBlack::testGetUninterpretedSortParamSorts() +{ + Sort uSort = d_solver.mkUninterpretedSort("u"); + TS_ASSERT_THROWS_NOTHING(uSort.getUninterpretedSortParamSorts()); + Sort bvSort = d_solver.mkBitVectorSort(32); + TS_ASSERT_THROWS(bvSort.getUninterpretedSortParamSorts(), CVC4ApiException&); +} + +void SortBlack::testGetUninterpretedSortConstructorName() +{ + Sort sSort = d_solver.mkSortConstructorSort("s", 2); + TS_ASSERT_THROWS_NOTHING(sSort.getSortConstructorName()); + Sort bvSort = d_solver.mkBitVectorSort(32); + TS_ASSERT_THROWS(bvSort.getSortConstructorName(), CVC4ApiException&); +} + +void SortBlack::testGetUninterpretedSortConstructorArity() +{ + Sort sSort = d_solver.mkSortConstructorSort("s", 2); + TS_ASSERT_THROWS_NOTHING(sSort.getSortConstructorArity()); + Sort bvSort = d_solver.mkBitVectorSort(32); + TS_ASSERT_THROWS(bvSort.getSortConstructorArity(), CVC4ApiException&); +} + +void SortBlack::testGetBVSize() +{ + Sort bvSort = d_solver.mkBitVectorSort(32); + TS_ASSERT_THROWS_NOTHING(bvSort.getBVSize()); + Sort setSort = d_solver.mkSetSort(d_solver.getIntegerSort()); + TS_ASSERT_THROWS(setSort.getBVSize(), CVC4ApiException&); +} + +void SortBlack::testGetFPExponentSize() +{ + Sort fpSort = d_solver.mkFloatingPointSort(4, 8); + TS_ASSERT_THROWS_NOTHING(fpSort.getFPExponentSize()); + Sort setSort = d_solver.mkSetSort(d_solver.getIntegerSort()); + TS_ASSERT_THROWS(setSort.getFPExponentSize(), CVC4ApiException&); +} + +void SortBlack::testGetFPSignificandSize() +{ + Sort fpSort = d_solver.mkFloatingPointSort(4, 8); + TS_ASSERT_THROWS_NOTHING(fpSort.getFPSignificandSize()); + Sort setSort = d_solver.mkSetSort(d_solver.getIntegerSort()); + TS_ASSERT_THROWS(setSort.getFPSignificandSize(), CVC4ApiException&); +} + +void SortBlack::testGetDatatypeParamSorts() +{ + // create parametric datatype, check should not fail + Sort sort = d_solver.mkParamSort("T"); + DatatypeDecl paramDtypeSpec("paramlist", sort); + DatatypeConstructorDecl paramCons("cons"); + DatatypeConstructorDecl paramNil("nil"); + DatatypeSelectorDecl paramHead("head", sort); + paramCons.addSelector(paramHead); + paramDtypeSpec.addConstructor(paramCons); + paramDtypeSpec.addConstructor(paramNil); + Sort paramDtypeSort = d_solver.mkDatatypeSort(paramDtypeSpec); + TS_ASSERT_THROWS_NOTHING(paramDtypeSort.getDatatypeParamSorts()); + // create non-parametric datatype sort, check should fail + DatatypeDecl dtypeSpec("list"); + DatatypeConstructorDecl cons("cons"); + DatatypeSelectorDecl head("head", d_solver.getIntegerSort()); + cons.addSelector(head); + dtypeSpec.addConstructor(cons); + DatatypeConstructorDecl nil("nil"); + dtypeSpec.addConstructor(nil); + Sort dtypeSort = d_solver.mkDatatypeSort(dtypeSpec); + TS_ASSERT_THROWS(dtypeSort.getDatatypeParamSorts(), CVC4ApiException&); +} + +void SortBlack::testGetDatatypeArity() +{ + // create datatype sort, check should not fail + DatatypeDecl dtypeSpec("list"); + DatatypeConstructorDecl cons("cons"); + DatatypeSelectorDecl head("head", d_solver.getIntegerSort()); + cons.addSelector(head); + dtypeSpec.addConstructor(cons); + DatatypeConstructorDecl nil("nil"); + dtypeSpec.addConstructor(nil); + Sort dtypeSort = d_solver.mkDatatypeSort(dtypeSpec); + TS_ASSERT_THROWS_NOTHING(dtypeSort.getDatatypeArity()); + // create bv sort, check should fail + Sort bvSort = d_solver.mkBitVectorSort(32); + TS_ASSERT_THROWS(bvSort.getDatatypeArity(), CVC4ApiException&); +} + +void SortBlack::testGetTupleLength() +{ + Sort tupleSort = d_solver.mkTupleSort( + {d_solver.getIntegerSort(), d_solver.getIntegerSort()}); + TS_ASSERT_THROWS_NOTHING(tupleSort.getTupleLength()); + Sort bvSort = d_solver.mkBitVectorSort(32); + TS_ASSERT_THROWS(bvSort.getTupleLength(), CVC4ApiException&); +} + +void SortBlack::testGetTupleSorts() +{ + Sort tupleSort = d_solver.mkTupleSort( + {d_solver.getIntegerSort(), d_solver.getIntegerSort()}); + TS_ASSERT_THROWS_NOTHING(tupleSort.getTupleSorts()); + Sort bvSort = d_solver.mkBitVectorSort(32); + TS_ASSERT_THROWS(bvSort.getTupleSorts(), CVC4ApiException&); +} diff --git a/test/unit/api/term_black.h b/test/unit/api/term_black.h new file mode 100644 index 000000000..c2ca1cb08 --- /dev/null +++ b/test/unit/api/term_black.h @@ -0,0 +1,37 @@ +/********************* */ +/*! \file term_black.h + ** \verbatim + ** Top contributors (to current version): + ** Andres Noetzli + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS + ** in the top-level source directory) and their institutional affiliations. + ** All rights reserved. See the file COPYING in the top-level source + ** directory for licensing information.\endverbatim + ** + ** \brief Black box testing of the Term class + **/ + +#include <cxxtest/TestSuite.h> + +#include "api/cvc4cpp.h" + +using namespace CVC4::api; + +class TermBlack : public CxxTest::TestSuite +{ + public: + void setUp() override {} + void tearDown() override {} + + void testTermAssignment() + { + Term t1 = d_solver.mkReal(1); + Term t2 = t1; + t2 = d_solver.mkReal(2); + TS_ASSERT_EQUALS(t1, d_solver.mkReal(1)); + } + + private: + Solver d_solver; +}; diff --git a/test/unit/theory/theory_strings_rewriter_white.h b/test/unit/theory/theory_strings_rewriter_white.h index 87aef3704..42ac2cdd9 100644 --- a/test/unit/theory/theory_strings_rewriter_white.h +++ b/test/unit/theory/theory_strings_rewriter_white.h @@ -604,6 +604,18 @@ class TheoryStringsRewriterWhite : public CxxTest::TestSuite b); repl = d_nm->mkNode(kind::STRING_STRREPL, b, x, b); sameNormalForm(repl_repl, repl); + + // Different normal forms for: + // + // (str.replace "B" (str.replace "" x "A") "B") + // + // (str.replace "B" x "B") + repl_repl = d_nm->mkNode(kind::STRING_STRREPL, + b, + d_nm->mkNode(kind::STRING_STRREPL, empty, x, a), + b); + repl = d_nm->mkNode(kind::STRING_STRREPL, b, x, b); + differentNormalForms(repl_repl, repl); } void testRewriteContains() |