From 6beb70fcedd18e965ad82949090365cb44a43692 Mon Sep 17 00:00:00 2001 From: Abdalrhman Mohamed <32971963+abdoo8080@users.noreply.github.com> Date: Tue, 23 Mar 2021 09:44:39 -0500 Subject: [PATCH] Replace old sygus term reconstruction algorithm with a new one. (#5779) This PR replaces the old algorithm for reconstructing sygus terms with a new "proper" implementation. --- src/CMakeLists.txt | 8 +- src/expr/node.h | 16 + .../quantifiers/candidate_rewrite_database.h | 5 +- .../sygus/ce_guided_single_inv.cpp | 39 +- .../quantifiers/sygus/ce_guided_single_inv.h | 17 +- .../sygus/ce_guided_single_inv_sol.cpp | 1055 ----------------- .../sygus/ce_guided_single_inv_sol.h | 205 ---- .../sygus/rcons_obligation_info.cpp | 100 ++ .../quantifiers/sygus/rcons_obligation_info.h | 150 +++ .../quantifiers/sygus/rcons_type_info.cpp | 72 ++ .../quantifiers/sygus/rcons_type_info.h | 102 ++ .../quantifiers/sygus/sygus_reconstruct.cpp | 491 ++++++++ .../quantifiers/sygus/sygus_reconstruct.h | 312 +++++ .../quantifiers/sygus/synth_conjecture.cpp | 14 +- .../quantifiers/sygus/synth_conjecture.h | 5 +- test/regress/CMakeLists.txt | 21 +- test/regress/regress1/sygus/array_search_2.sy | 2 +- .../regress1/sygus/complex-no-rewrite.sy | 21 + .../regress1/sygus/complex-rewrite-in-db.sy | 21 + test/regress/regress1/sygus/no-var-in-sol.sy | 24 + .../regress1/sygus/simple-no-rewrite.sy | 15 + .../regress1/sygus/simple-not-in-grammar.sy | 12 + .../regress1/sygus/simple-rewrite-in-db.sy | 15 + .../sygus/simple-rewrite-not-in-db.sy | 16 + 24 files changed, 1431 insertions(+), 1307 deletions(-) delete mode 100644 src/theory/quantifiers/sygus/ce_guided_single_inv_sol.cpp delete mode 100644 src/theory/quantifiers/sygus/ce_guided_single_inv_sol.h create mode 100644 src/theory/quantifiers/sygus/rcons_obligation_info.cpp create mode 100644 src/theory/quantifiers/sygus/rcons_obligation_info.h create mode 100644 src/theory/quantifiers/sygus/rcons_type_info.cpp create mode 100644 src/theory/quantifiers/sygus/rcons_type_info.h create mode 100644 src/theory/quantifiers/sygus/sygus_reconstruct.cpp create mode 100644 src/theory/quantifiers/sygus/sygus_reconstruct.h create mode 100644 test/regress/regress1/sygus/complex-no-rewrite.sy create mode 100644 test/regress/regress1/sygus/complex-rewrite-in-db.sy create mode 100644 test/regress/regress1/sygus/no-var-in-sol.sy create mode 100644 test/regress/regress1/sygus/simple-no-rewrite.sy create mode 100644 test/regress/regress1/sygus/simple-not-in-grammar.sy create mode 100644 test/regress/regress1/sygus/simple-rewrite-in-db.sy create mode 100644 test/regress/regress1/sygus/simple-rewrite-not-in-db.sy diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt index 54ece796a..5b7c1d8f8 100644 --- a/src/CMakeLists.txt +++ b/src/CMakeLists.txt @@ -777,8 +777,6 @@ libcvc4_add_sources( theory/quantifiers/term_tuple_enumerator.h theory/quantifiers/sygus/ce_guided_single_inv.cpp theory/quantifiers/sygus/ce_guided_single_inv.h - theory/quantifiers/sygus/ce_guided_single_inv_sol.cpp - theory/quantifiers/sygus/ce_guided_single_inv_sol.h theory/quantifiers/sygus/cegis.cpp theory/quantifiers/sygus/cegis.h theory/quantifiers/sygus/cegis_core_connective.cpp @@ -797,6 +795,10 @@ libcvc4_add_sources( theory/quantifiers/sygus/example_infer.h theory/quantifiers/sygus/example_min_eval.cpp theory/quantifiers/sygus/example_min_eval.h + theory/quantifiers/sygus/rcons_obligation_info.cpp + theory/quantifiers/sygus/rcons_obligation_info.h + theory/quantifiers/sygus/rcons_type_info.cpp + theory/quantifiers/sygus/rcons_type_info.h theory/quantifiers/sygus/sygus_abduct.cpp theory/quantifiers/sygus/sygus_abduct.h theory/quantifiers/sygus/sygus_enumerator.cpp @@ -823,6 +825,8 @@ libcvc4_add_sources( theory/quantifiers/sygus/sygus_pbe.h theory/quantifiers/sygus/sygus_process_conj.cpp theory/quantifiers/sygus/sygus_process_conj.h + theory/quantifiers/sygus/sygus_reconstruct.cpp + theory/quantifiers/sygus/sygus_reconstruct.h theory/quantifiers/sygus/sygus_qe_preproc.cpp theory/quantifiers/sygus/sygus_qe_preproc.h theory/quantifiers/sygus/sygus_repair_const.cpp diff --git a/src/expr/node.h b/src/expr/node.h index bb8c5618c..9e485ae78 100644 --- a/src/expr/node.h +++ b/src/expr/node.h @@ -513,6 +513,12 @@ public: Node substitute(Iterator substitutionsBegin, Iterator substitutionsEnd) const; + /** + * Simultaneous substitution of Nodes in cache. + */ + Node substitute( + std::unordered_map& cache) const; + /** * Returns the kind of this node. * @return the kind @@ -1380,6 +1386,16 @@ NodeTemplate::substitute(Iterator substitutionsBegin, return substitute(substitutionsBegin, substitutionsEnd, cache); } +template +inline Node NodeTemplate::substitute( + std::unordered_map& cache) const +{ + // Since no substitution is given (other than what may already be in the + // cache), we pass dummy iterators to conform to the main substitute method, + // giving the same value to substitutionsBegin and substitutionsEnd. + return substitute(cache.cend(), cache.cend(), cache); +} + template template Node diff --git a/src/theory/quantifiers/candidate_rewrite_database.h b/src/theory/quantifiers/candidate_rewrite_database.h index a5fb33a1f..3313b507b 100644 --- a/src/theory/quantifiers/candidate_rewrite_database.h +++ b/src/theory/quantifiers/candidate_rewrite_database.h @@ -58,8 +58,7 @@ class CandidateRewriteDatabase : public ExprMiner bool filterPairs = true); ~CandidateRewriteDatabase() {} /** Initialize this class */ - void initialize(const std::vector& var, - SygusSampler* ss = nullptr) override; + void initialize(const std::vector& var, SygusSampler* ss) override; /** Initialize this class * * Serves the same purpose as the above function, but we will be using @@ -75,7 +74,7 @@ class CandidateRewriteDatabase : public ExprMiner void initializeSygus(const std::vector& vars, QuantifiersEngine* qe, Node f, - SygusSampler* ss = nullptr); + SygusSampler* ss); /** add term * * Notifies this class that the solution sol was enumerated. This may diff --git a/src/theory/quantifiers/sygus/ce_guided_single_inv.cpp b/src/theory/quantifiers/sygus/ce_guided_single_inv.cpp index 3e223fd7c..f93260f0c 100644 --- a/src/theory/quantifiers/sygus/ce_guided_single_inv.cpp +++ b/src/theory/quantifiers/sygus/ce_guided_single_inv.cpp @@ -23,6 +23,7 @@ #include "theory/quantifiers/quantifiers_attributes.h" #include "theory/quantifiers/quantifiers_rewriter.h" #include "theory/quantifiers/sygus/sygus_grammar_cons.h" +#include "theory/quantifiers/sygus/sygus_reconstruct.h" #include "theory/quantifiers/sygus/sygus_utils.h" #include "theory/quantifiers/sygus/term_database_sygus.h" #include "theory/quantifiers/term_enumeration.h" @@ -37,19 +38,17 @@ namespace CVC4 { namespace theory { namespace quantifiers { -CegSingleInv::CegSingleInv(QuantifiersEngine* qe) +CegSingleInv::CegSingleInv(QuantifiersEngine* qe, SygusStatistics& s) : d_qe(qe), d_sip(new SingleInvocationPartition), - d_sol(new CegSingleInvSol(qe)), + d_srcons(new SygusReconstruct(qe->getTermDatabaseSygus(), s)), d_isSolved(false), d_single_invocation(false) { - } CegSingleInv::~CegSingleInv() { - delete d_sol; // (new CegSingleInvSol(qe)), delete d_sip; // d_sip(new SingleInvocationPartition), } @@ -296,7 +295,7 @@ struct sortSiInstanceIndices { Node CegSingleInv::getSolution(size_t sol_index, TypeNode stn, - int& reconstructed, + int8_t& reconstructed, bool rconsSygus) { Assert(sol_index < d_quant[0].getNumChildren()); @@ -316,21 +315,18 @@ Node CegSingleInv::getSolution(size_t sol_index, // must substitute to be proper variables const DType& dt = stn.getDType(); Node varList = dt.getSygusVarList(); - d_sol->d_varList.clear(); Assert(d_single_inv_arg_sk.size() == varList.getNumChildren()); - std::vector< Node > vars; + std::vector vars; + std::vector sygusVars; for (size_t i = 0, nvars = d_single_inv_arg_sk.size(); i < nvars; i++) { Trace("csi-sol") << d_single_inv_arg_sk[i] << " "; vars.push_back(d_single_inv_arg_sk[i]); - d_sol->d_varList.push_back(varList[i]); + sygusVars.push_back(varList[i]); } Trace("csi-sol") << std::endl; - Assert(vars.size() == d_sol->d_varList.size()); - sol = sol.substitute(vars.begin(), - vars.end(), - d_sol->d_varList.begin(), - d_sol->d_varList.end()); + sol = sol.substitute( + vars.begin(), vars.end(), sygusVars.begin(), sygusVars.end()); sol = reconstructToSyntax(sol, stn, reconstructed, rconsSygus); return s.getKind() == LAMBDA ? NodeManager::currentNM()->mkNode(LAMBDA, s[0], sol) @@ -339,7 +335,6 @@ Node CegSingleInv::getSolution(size_t sol_index, Node CegSingleInv::getSolutionFromInst(size_t index) { - Assert(d_sol != NULL); Node prog = d_quant[0][index]; Node s; // If it is unconstrained: either the variable does not appear in the @@ -431,21 +426,20 @@ void CegSingleInv::setSolution() Node CegSingleInv::reconstructToSyntax(Node s, TypeNode stn, - int& reconstructed, + int8_t& reconstructed, bool rconsSygus) { // extract the lambda body Node sol = s; const DType& dt = stn.getDType(); - //reconstruct the solution into sygus if necessary + // reconstruct the solution into sygus if necessary reconstructed = 0; if (options::cegqiSingleInvReconstruct() != options::CegqiSingleInvRconsMode::NONE && !dt.getSygusAllowAll() && !stn.isNull() && rconsSygus) { - d_sol->preregisterConjecture( d_orig_conjecture ); - int enumLimit = -1; + int64_t enumLimit = -1; if (options::cegqiSingleInvReconstruct() == options::CegqiSingleInvRconsMode::TRY) { @@ -456,12 +450,15 @@ Node CegSingleInv::reconstructToSyntax(Node s, { enumLimit = options::cegqiSingleInvReconstructLimit(); } - sol = d_sol->reconstructSolution(s, stn, reconstructed, enumLimit); - if( reconstructed==1 ){ + sol = d_srcons->reconstructSolution(s, stn, reconstructed, enumLimit); + if (reconstructed == 1) + { Trace("csi-sol") << "Solution (post-reconstruction into Sygus): " << sol << std::endl; } - }else{ + } + else + { Trace("csi-sol") << "Post-process solution..." << std::endl; Node prev = sol; sol = d_qe->getTermDatabaseSygus()->getExtRewriter()->extendedRewrite(sol); diff --git a/src/theory/quantifiers/sygus/ce_guided_single_inv.h b/src/theory/quantifiers/sygus/ce_guided_single_inv.h index a650a58a9..c73954195 100644 --- a/src/theory/quantifiers/sygus/ce_guided_single_inv.h +++ b/src/theory/quantifiers/sygus/ce_guided_single_inv.h @@ -22,13 +22,14 @@ #include "theory/quantifiers/cegqi/inst_strategy_cegqi.h" #include "theory/quantifiers/inst_match_trie.h" #include "theory/quantifiers/single_inv_partition.h" -#include "theory/quantifiers/sygus/ce_guided_single_inv_sol.h" +#include "theory/quantifiers/sygus/sygus_stats.h" namespace CVC4 { namespace theory { namespace quantifiers { class SynthConjecture; +class SygusReconstruct; // this class infers whether a conjecture is single invocation (Reynolds et al CAV 2015), and sets up the // counterexample-guided quantifier instantiation utility (d_cinst), and methods for solution @@ -53,8 +54,8 @@ class CegSingleInv QuantifiersEngine* d_qe; // single invocation inference utility SingleInvocationPartition* d_sip; - // solution reconstruction - CegSingleInvSol* d_sol; + /** solution reconstruction */ + std::unique_ptr d_srcons; // list of skolems for each argument of programs std::vector d_single_inv_arg_sk; @@ -91,7 +92,7 @@ class CegSingleInv Node d_single_inv; public: - CegSingleInv(QuantifiersEngine* qe); + CegSingleInv(QuantifiersEngine* qe, SygusStatistics& s); ~CegSingleInv(); // get simplified conjecture @@ -132,11 +133,13 @@ class CegSingleInv */ Node getSolution(size_t sol_index, TypeNode stn, - int& reconstructed, + int8_t& reconstructed, bool rconsSygus = true); //reconstruct to syntax - Node reconstructToSyntax( Node s, TypeNode stn, int& reconstructed, - bool rconsSygus = true ); + Node reconstructToSyntax(Node s, + TypeNode stn, + int8_t& reconstructed, + bool rconsSygus = true); // is single invocation bool isSingleInvocation() const { return !d_single_inv.isNull(); } /** preregister conjecture */ diff --git a/src/theory/quantifiers/sygus/ce_guided_single_inv_sol.cpp b/src/theory/quantifiers/sygus/ce_guided_single_inv_sol.cpp deleted file mode 100644 index 509e4905e..000000000 --- a/src/theory/quantifiers/sygus/ce_guided_single_inv_sol.cpp +++ /dev/null @@ -1,1055 +0,0 @@ -/********************* */ -/*! \file ce_guided_single_inv_sol.cpp - ** \verbatim - ** Top contributors (to current version): - ** Andrew Reynolds, Tim King, Mathias Preiner - ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2021 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 utility for processing single invocation synthesis conjectures - ** - **/ -#include "theory/quantifiers/sygus/ce_guided_single_inv_sol.h" - -#include "expr/dtype.h" -#include "expr/dtype_cons.h" -#include "expr/node_algorithm.h" -#include "options/quantifiers_options.h" -#include "smt/command.h" -#include "theory/arith/arith_msum.h" -#include "theory/quantifiers/ematching/trigger.h" -#include "theory/quantifiers/first_order_model.h" -#include "theory/quantifiers/quantifiers_attributes.h" -#include "theory/quantifiers/sygus/ce_guided_single_inv.h" -#include "theory/quantifiers/sygus/synth_engine.h" -#include "theory/quantifiers/sygus/term_database_sygus.h" -#include "theory/quantifiers/term_enumeration.h" -#include "theory/quantifiers/term_util.h" -#include "theory/quantifiers_engine.h" -#include "theory/rewriter.h" - -using namespace CVC4::kind; -using namespace std; - -namespace CVC4 { -namespace theory { -namespace quantifiers { - -bool doCompare(Node a, Node b, Kind k) -{ - Node com = NodeManager::currentNM()->mkNode(k, a, b); - com = Rewriter::rewrite(com); - Assert(com.getType().isBoolean()); - return com.isConst() && com.getConst(); -} - -CegSingleInvSol::CegSingleInvSol(QuantifiersEngine* qe) - : d_qe(qe), d_id_count(0), d_root_id() -{ -} - -void CegSingleInvSol::preregisterConjecture(Node q) -{ - Trace("csi-sol") << "Preregister conjecture : " << q << std::endl; - Node n = q; - if( n.getKind()==FORALL ){ - n = n[1]; - } - if( n.getKind()==EXISTS ){ - if( n[0].getNumChildren()==d_varList.size() ){ - std::vector< Node > evars; - for( unsigned i=0; i >::iterator it = - d_rcons_to_id.begin(); - it != d_rcons_to_id.end(); - ++it) - { - TypeNode tn = it->first; - Assert(tn.isDatatype()); - const DType& dt = tn.getDType(); - Trace("csi-rcons") << "Terms to reconstruct of type " << dt.getName() - << " : " << std::endl; - for (std::map::iterator it2 = it->second.begin(); - it2 != it->second.end(); - ++it2) - { - if (d_reconstruct.find(it2->second) == d_reconstruct.end()) - { - Trace("csi-rcons") << " " << it2->first << std::endl; - } - } - Assert(!it->second.empty()); - } - } - if (enumLimit != 0) - { - int index = 0; - std::map< TypeNode, bool > active; - for( std::map< TypeNode, std::map< Node, int > >::iterator it = d_rcons_to_id.begin(); it != d_rcons_to_id.end(); ++it ){ - active[it->first] = true; - } - //enumerate for all types - do { - std::vector< TypeNode > to_erase; - for( std::map< TypeNode, bool >::iterator it = active.begin(); it != active.end(); ++it ){ - TypeNode tn = it->first; - Node ns = d_qe->getTermEnumeration()->getEnumerateTerm(tn, index); - if( ns.isNull() ){ - to_erase.push_back(tn); - }else{ - Node nb = d_qe->getTermDatabaseSygus()->sygusToBuiltin(ns, tn); - Node nr = Rewriter::rewrite(nb); // d_qe->getTermDatabaseSygus()->getNormalized( - // tn, nb, false, false ); - Trace("csi-rcons-debug2") - << " - try " << ns << " -> " << nr << " for " << tn << " " - << nr.getKind() << std::endl; - std::map::iterator itt = d_rcons_to_id[tn].find(nr); - if (itt != d_rcons_to_id[tn].end()) - { - // if it is not already reconstructed - if (d_reconstruct.find(itt->second) == d_reconstruct.end()) - { - Trace("csi-rcons") << "...reconstructed " << ns << " for term " - << nr << std::endl; - setReconstructed(itt->second, ns); - Trace("csi-rcons-debug") - << "...path to root, try reconstruction." << std::endl; - d_tmp_fail.clear(); - Node ret = getReconstructedSolution(d_root_id); - if (!ret.isNull()) - { - Trace("csi-rcons") - << "Sygus solution (after enumeration) is : " << ret - << std::endl; - reconstructed = 1; - return ret; - } - } - } - } - } - for( unsigned i=0; i::iterator itri = d_rcons_to_status[stn].find( t ); - if( itri!=d_rcons_to_status[stn].end() ){ - status = itri->second; - //Trace("csi-rcons-debug") << "-> (cached) " << status << " for " << d_rcons_to_id[stn][t] << std::endl; - return d_rcons_to_id[stn][t]; - }else{ - status = 1; - // register the type - registerType(stn); - int id = allocate( t, stn ); - d_rcons_to_status[stn][t] = -1; - TypeNode tn = t.getType(); - Assert(stn.isDatatype()); - const DType& dt = stn.getDType(); - TermDbSygus* tds = d_qe->getTermDatabaseSygus(); - SygusTypeInfo& sti = tds->getTypeInfo(stn); - Assert(dt.isSygus()); - Trace("csi-rcons-debug") << "Check reconstruct " << t << ", sygus type " << dt.getName() << ", kind " << t.getKind() << ", id : " << id << std::endl; - int carg = -1; - int karg = -1; - // first, do standard minimizations - Node min_t = minimizeBuiltinTerm(t); - Trace("csi-rcons-debug") << "Minimized term is : " << min_t << std::endl; - //check if op is in syntax sort - - carg = sti.getOpConsNum(min_t); - if( carg!=-1 ){ - Trace("csi-rcons-debug") << " Type has operator." << std::endl; - d_reconstruct[id] = NodeManager::currentNM()->mkNode( - APPLY_CONSTRUCTOR, dt[carg].getConstructor()); - status = 0; - }else{ - //check if kind is in syntax sort - karg = sti.getKindConsNum(min_t.getKind()); - if( karg!=-1 ){ - //collect the children of min_t - std::vector< Node > tchildren; - if( min_t.getNumChildren()>dt[karg].getNumArgs() && quantifiers::TermUtil::isAssoc( min_t.getKind() ) && dt[karg].getNumArgs()==2 ){ - tchildren.push_back( min_t[0] ); - std::vector< Node > rem_children; - for( unsigned i=1; imkNode( min_t.getKind(), rem_children ); - tchildren.push_back( t2 ); - Trace("csi-rcons-debug") << "...split n-ary to binary " << min_t[0] << " " << t2 << "." << std::endl; - }else{ - for( unsigned i=0; i args; - if (getMatch(min_t, stn, index_found, args, karg, c_index)) - { - success = true; - status = 0; - Node cons = dt[index_found].getConstructor(); - Trace("csi-rcons-debug") << "Try alternative for " << id << ", matching " << dt[index_found].getName() << " with children : " << std::endl; - for( unsigned i=0; i equiv; - if( tn.isBoolean() ){ - Node curr = min_t; - Node new_t; - do{ - new_t = Node::null(); - if( curr.getKind()==EQUAL ){ - if( curr[0].getType().isInteger() || curr[0].getType().isReal() ){ - new_t = NodeManager::currentNM()->mkNode( AND, NodeManager::currentNM()->mkNode( LEQ, curr[0], curr[1] ), - NodeManager::currentNM()->mkNode( LEQ, curr[1], curr[0] ) ); - }else if( curr[0].getType().isBoolean() ){ - new_t = NodeManager::currentNM()->mkNode( OR, NodeManager::currentNM()->mkNode( AND, curr[0], curr[1] ), - NodeManager::currentNM()->mkNode( AND, curr[0].negate(), curr[1].negate() ) ); - }else{ - new_t = NodeManager::currentNM()->mkNode( NOT, NodeManager::currentNM()->mkNode( NOT, curr ) ); - } - }else if( curr.getKind()==ITE ){ - new_t = NodeManager::currentNM()->mkNode( OR, NodeManager::currentNM()->mkNode( AND, curr[0], curr[1] ), - NodeManager::currentNM()->mkNode( AND, curr[0].negate(), curr[2] ) ); - }else if( curr.getKind()==OR || curr.getKind()==AND ){ - new_t = TermUtil::simpleNegate( curr ).negate(); - }else if( curr.getKind()==NOT ){ - new_t = TermUtil::simpleNegate( curr[0] ); - }else{ - new_t = NodeManager::currentNM()->mkNode( NOT, NodeManager::currentNM()->mkNode( NOT, curr ) ); - } - if( !new_t.isNull() ){ - if( new_t!=min_t && std::find( equiv.begin(), equiv.end(), new_t )==equiv.end() ){ - curr = new_t; - equiv.push_back( new_t ); - }else{ - new_t = Node::null(); - } - } - }while( !new_t.isNull() ); - } - //get decompositions - for( unsigned i=0; i equiv_ids; - for( unsigned i=0; i *** reconstruction required for id " << id << std::endl; - }else{ - Trace("csi-rcons-debug") << "-> success for " << id << std::endl; - } - d_rcons_to_status[stn][t] = status; - return id; - } -} - -bool CegSingleInvSol::collectReconstructNodes(int pid, - std::vector& ts, - const DTypeConstructor& dtc, - std::vector& ids, - int& status) -{ - Assert(dtc.getNumArgs() == ts.size()); - for( unsigned i=0; igetTermDatabaseSygus()->getArgType( dtc, i ); - int cstatus; - int c_id = collectReconstructNodes( ts[i], cstn, cstatus ); - if( cstatus==-1 ){ - return false; - }else if( cstatus!=0 ){ - status = 1; - } - ids.push_back( c_id ); - } - for( unsigned i=0; i::iterator it = d_reconstruct.find( id ); - if( it!=d_reconstruct.end() ){ - return it->second; - }else{ - if( std::find( d_tmp_fail.begin(), d_tmp_fail.end(), id )!=d_tmp_fail.end() ){ - return Node::null(); - }else{ - // try each child option - std::map< int, std::map< Node, std::vector< int > > >::iterator ito = d_reconstruct_op.find( id ); - if( ito!=d_reconstruct_op.end() ){ - for( std::map< Node, std::vector< int > >::iterator itt = ito->second.begin(); itt != ito->second.end(); ++itt ){ - std::vector< Node > children; - children.push_back( itt->first ); - bool success = true; - for( unsigned i=0; isecond.size(); i++ ){ - Node nc = getReconstructedSolution( itt->second[i] ); - if( nc.isNull() ){ - success = false; - break; - }else{ - children.push_back( nc ); - } - } - if( success ){ - Node ret = NodeManager::currentNM()->mkNode( APPLY_CONSTRUCTOR, children ); - setReconstructed( id, ret ); - return ret; - } - } - } - // try terms in the equivalence class of this - if( mod_eq ){ - int rid = d_rep[id]; - for( unsigned i=0; i::iterator it = d_rcons_to_id[stn].find( n ); - if( it==d_rcons_to_id[stn].end() ){ - int ret = d_id_count; - if( Trace.isOn("csi-rcons-debug") ){ - const DType& dt = stn.getDType(); - Trace("csi-rcons-debug") << "id " << ret << " : " << n << " " << dt.getName() << std::endl; - } - d_id_node[d_id_count] = n; - d_id_type[d_id_count] = stn; - d_rep[d_id_count] = d_id_count; - d_eqc[d_id_count].push_back( d_id_count ); - d_rcons_to_id[stn][n] = d_id_count; - d_id_count++; - return ret; - }else{ - return it->second; - } -} - -bool CegSingleInvSol::getPathToRoot(int id) -{ - if( id==d_root_id ){ - return true; - }else{ - std::map< int, Node >::iterator it = d_reconstruct.find( id ); - if( it!=d_reconstruct.end() ){ - return false; - }else{ - int rid = d_rep[id]; - for( unsigned j=0; j& equiv) -{ - if( k==AND || k==OR ){ - equiv.push_back( NodeManager::currentNM()->mkNode( k, n, n ) ); - equiv.push_back( NodeManager::currentNM()->mkNode( k, n, NodeManager::currentNM()->mkConst( k==AND ) ) ); - } - //multiplication for integers - //TODO for bitvectors - Kind mk = ( k==PLUS || k==MINUS ) ? MULT : UNDEFINED_KIND; - if( mk!=UNDEFINED_KIND ){ - if( n.getKind()==mk && n[0].isConst() && n[0].getType().isInteger() ){ - bool success = true; - for( unsigned i=0; i<2; i++ ){ - Node eq; - if( k==PLUS || k==MINUS ){ - Node oth = NodeManager::currentNM()->mkConst( Rational(i==0 ? 1000 : -1000) ); - eq = i==0 ? NodeManager::currentNM()->mkNode( LEQ, n[0], oth ) : NodeManager::currentNM()->mkNode( GEQ, n[0], oth ); - } - if( !eq.isNull() ){ - eq = Rewriter::rewrite( eq ); - if (!eq.isConst() || !eq.getConst()) - { - success = false; - break; - } - } - } - if( success ){ - Node var = n[1]; - Node rem; - if( k==PLUS || k==MINUS ){ - int rem_coeff = (int)n[0].getConst().getNumerator().getSignedInt(); - if( rem_coeff>0 && k==PLUS ){ - rem_coeff--; - }else if( rem_coeff<0 && k==MINUS ){ - rem_coeff++; - }else{ - success = false; - } - if( success ){ - rem = NodeManager::currentNM()->mkNode( MULT, NodeManager::currentNM()->mkConst( Rational(rem_coeff) ), var ); - rem = Rewriter::rewrite( rem ); - } - } - if( !rem.isNull() ){ - equiv.push_back( NodeManager::currentNM()->mkNode( k, rem, var ) ); - } - } - } - } - //negative constants - if( k==MINUS ){ - if( n.isConst() && n.getType().isInteger() && n.getConst().getNumerator().strictlyNegative() ){ - Node nn = NodeManager::currentNM()->mkNode( UMINUS, n ); - nn = Rewriter::rewrite( nn ); - equiv.push_back( NodeManager::currentNM()->mkNode( MINUS, NodeManager::currentNM()->mkConst( Rational(0) ), nn ) ); - } - } - //inequalities - if( k==GEQ || k==LEQ || k==LT || k==GT || k==NOT ){ - Node atom = n.getKind()==NOT ? n[0] : n; - bool pol = n.getKind()!=NOT; - Kind ak = atom.getKind(); - if( ( ak==GEQ || ak==LEQ || ak==LT || ak==GT ) && ( pol || k!=NOT ) ){ - Node t1 = atom[0]; - Node t2 = atom[1]; - if( !pol ){ - ak = ak==GEQ ? LT : ( ak==LEQ ? GT : ( ak==LT ? GEQ : LEQ ) ); - } - if( k==NOT ){ - equiv.push_back( NodeManager::currentNM()->mkNode( ak==GEQ ? LT : ( ak==LEQ ? GT : ( ak==LT ? GEQ : LEQ ) ), t1, t2 ).negate() ); - }else if( k==ak ){ - equiv.push_back( NodeManager::currentNM()->mkNode( k, t1, t2 ) ); - }else if( (k==GEQ || k==LEQ)==(ak==GEQ || ak==LEQ) ){ - equiv.push_back( NodeManager::currentNM()->mkNode( k, t2, t1 ) ); - }else if( t1.getType().isInteger() && t2.getType().isInteger() ){ - if( (k==GEQ || k==GT)!=(ak==GEQ || ak==GT) ){ - Node ts = t1; - t1 = t2; - t2 = ts; - ak = ak==GEQ ? LEQ : ( ak==LEQ ? GEQ : ( ak==LT ? GT : LT ) ); - } - t2 = NodeManager::currentNM()->mkNode( PLUS, t2, NodeManager::currentNM()->mkConst( Rational( (ak==GT || ak==LEQ) ? 1 : -1 ) ) ); - t2 = Rewriter::rewrite( t2 ); - equiv.push_back( NodeManager::currentNM()->mkNode( k, t1, t2 ) ); - } - } - } - - //based on eqt cache - std::map< Node, Node >::iterator itet = d_eqt_rep.find( n ); - if( itet!=d_eqt_rep.end() ){ - Node rn = itet->second; - for( unsigned i=0; i::iterator it = d_builtin_const_to_sygus[tn].find(c); - if (it != d_builtin_const_to_sygus[tn].end()) - { - return it->second; - } - TermDbSygus* tds = d_qe->getTermDatabaseSygus(); - NodeManager* nm = NodeManager::currentNM(); - SygusTypeInfo& ti = tds->getTypeInfo(tn); - Node sc; - d_builtin_const_to_sygus[tn][c] = sc; - Assert(c.isConst()); - if (!tn.isDatatype()) - { - // if we've traversed to a builtin type, simply return c - d_builtin_const_to_sygus[tn][c] = c; - return c; - } - const DType& dt = tn.getDType(); - Trace("csi-rcons-debug") << "Try to reconstruct " << c << " in " - << dt.getName() << std::endl; - if (!dt.isSygus()) - { - // if we've traversed to a builtin datatype type, simply return c - d_builtin_const_to_sygus[tn][c] = c; - return c; - } - // if we are not interested in reconstructing constants, or the grammar allows - // them, return a proxy - if (!options::cegqiSingleInvReconstructConst() || dt.getSygusAllowConst()) - { - sc = tds->getProxyVariable(tn, c); - } - else - { - int carg = ti.getOpConsNum(c); - if (carg != -1) - { - sc = nm->mkNode(APPLY_CONSTRUCTOR, dt[carg].getConstructor()); - } - else - { - // identity functions - for (unsigned ii : d_id_funcs[tn]) - { - Assert(dt[ii].getNumArgs() == 1); - // try to directly reconstruct from single argument - TypeNode tnc = tds->getArgType(dt[ii], 0); - Trace("csi-rcons-debug") - << "Based on id function " << dt[ii].getSygusOp() - << ", try reconstructing " << c << " instead in " << tnc - << std::endl; - Node n = builtinToSygusConst(c, tnc, rcons_depth); - if (!n.isNull()) - { - sc = nm->mkNode(APPLY_CONSTRUCTOR, dt[ii].getConstructor(), n); - break; - } - } - if (sc.isNull()) - { - if (rcons_depth < 1000) - { - // accelerated, recursive reconstruction of constants - Kind pk = getPlusKind(dt.getSygusType()); - if (pk != UNDEFINED_KIND) - { - int arg = ti.getKindConsNum(pk); - if (arg != -1) - { - Kind ck = getComparisonKind(dt.getSygusType()); - Kind pkm = getPlusKind(dt.getSygusType(), true); - // get types - Assert(dt[arg].getNumArgs() == 2); - TypeNode tn1 = tds->getArgType(dt[arg], 0); - TypeNode tn2 = tds->getArgType(dt[arg], 1); - // initialize d_const_list for tn1 - registerType(tn1); - // iterate over all positive constants, largest to smallest - int start = d_const_list[tn1].size() - 1; - int end = d_const_list[tn1].size() - d_const_list_pos[tn1]; - for (int i = start; i >= end; --i) - { - Node c1 = d_const_list[tn1][i]; - // only consider if smaller than c, and - if (doCompare(c1, c, ck)) - { - Node c2 = nm->mkNode(pkm, c, c1); - c2 = Rewriter::rewrite(c2); - if (c2.isConst()) - { - // reconstruct constant on the other side - Node sc2 = builtinToSygusConst(c2, tn2, rcons_depth + 1); - if (!sc2.isNull()) - { - Node sc1 = builtinToSygusConst(c1, tn1, rcons_depth); - Assert(!sc1.isNull()); - sc = nm->mkNode(APPLY_CONSTRUCTOR, - dt[arg].getConstructor(), - sc1, - sc2); - break; - } - } - } - } - } - } - } - } - } - } - d_builtin_const_to_sygus[tn][c] = sc; - return sc; -} - -struct sortConstants -{ - Kind d_comp_kind; - bool operator()(Node i, Node j) - { - return i != j && doCompare(i, j, d_comp_kind); - } -}; - -void CegSingleInvSol::registerType(TypeNode tn) -{ - if (d_const_list_pos.find(tn) != d_const_list_pos.end()) - { - return; - } - d_const_list_pos[tn] = 0; - Assert(tn.isDatatype()); - - TermDbSygus* tds = d_qe->getTermDatabaseSygus(); - // ensure it is registered - tds->registerSygusType(tn); - const DType& dt = tn.getDType(); - Assert(dt.isSygus()); - TypeNode btn = dt.getSygusType(); - // for constant reconstruction - Kind ck = getComparisonKind(btn); - Node z = TermUtil::mkTypeValue(btn, 0); - - // iterate over constructors - for (unsigned i = 0, ncons = dt.getNumConstructors(); i < ncons; i++) - { - Node n = dt[i].getSygusOp(); - if (n.getKind() != kind::BUILTIN && n.isConst()) - { - d_const_list[tn].push_back(n); - if (ck != UNDEFINED_KIND && doCompare(z, n, ck)) - { - d_const_list_pos[tn]++; - } - } - if (dt[i].isSygusIdFunc()) - { - d_id_funcs[tn].push_back(i); - } - } - // sort the constant list - if (!d_const_list[tn].empty()) - { - if (ck != UNDEFINED_KIND) - { - sortConstants sc; - sc.d_comp_kind = ck; - std::sort(d_const_list[tn].begin(), d_const_list[tn].end(), sc); - } - Trace("csi-rcons") << "Type has " << d_const_list[tn].size() - << " constants..." << std::endl - << " "; - for (unsigned i = 0; i < d_const_list[tn].size(); i++) - { - Trace("csi-rcons") << d_const_list[tn][i] << " "; - } - Trace("csi-rcons") << std::endl; - Trace("csi-rcons") << "Of these, " << d_const_list_pos[tn] - << " are marked as positive." << std::endl; - } -} - -bool CegSingleInvSol::getMatch(Node p, - Node n, - std::map& s, - std::vector& new_s) -{ - TermDbSygus* tds = d_qe->getTermDatabaseSygus(); - if (tds->isFreeVar(p)) - { - size_t vnum = tds->getFreeVarId(p); - Node prev = s[vnum]; - s[vnum] = n; - if (prev.isNull()) - { - new_s.push_back(vnum); - } - return prev.isNull() || prev == n; - } - if (n.getNumChildren() == 0) - { - return p == n; - } - if (n.getKind() == p.getKind() && n.getNumChildren() == p.getNumChildren()) - { - // try both ways? - unsigned rmax = - TermUtil::isComm(n.getKind()) && n.getNumChildren() == 2 ? 2 : 1; - std::vector new_tmp; - for (unsigned r = 0; r < rmax; r++) - { - bool success = true; - for (unsigned i = 0, size = n.getNumChildren(); i < size; i++) - { - int io = r == 0 ? i : (i == 0 ? 1 : 0); - if (!getMatch(p[i], n[io], s, new_tmp)) - { - success = false; - for (unsigned j = 0; j < new_tmp.size(); j++) - { - s.erase(new_tmp[j]); - } - new_tmp.clear(); - break; - } - } - if (success) - { - new_s.insert(new_s.end(), new_tmp.begin(), new_tmp.end()); - return true; - } - } - } - return false; -} - -bool CegSingleInvSol::getMatch(Node t, - TypeNode st, - int& index_found, - std::vector& args, - int index_exc, - int index_start) -{ - Assert(st.isDatatype()); - const DType& dt = st.getDType(); - Assert(dt.isSygus()); - std::map > kgens; - std::vector gens; - for (unsigned i = index_start, ncons = dt.getNumConstructors(); i < ncons; - i++) - { - if ((int)i != index_exc) - { - Node g = getGenericBase(st, dt, i); - gens.push_back(g); - kgens[g.getKind()].push_back(g); - Trace("csi-sol-debug") << "Check generic base : " << g << " from " - << dt[i].getName() << std::endl; - if (g.getKind() == t.getKind()) - { - Trace("csi-sol-debug") << "Possible match ? " << g << " " << t - << " for " << dt[i].getName() << std::endl; - std::map sigma; - std::vector new_s; - if (getMatch(g, t, sigma, new_s)) - { - // we found an exact match - bool msuccess = true; - for (unsigned j = 0, nargs = dt[i].getNumArgs(); j < nargs; j++) - { - if (sigma[j].isNull()) - { - msuccess = false; - break; - } - else - { - args.push_back(sigma[j]); - } - } - if (msuccess) - { - index_found = i; - return true; - } - } - } - } - } - return false; -} - -Node CegSingleInvSol::getGenericBase(TypeNode tn, const DType& dt, int c) -{ - std::map::iterator it = d_generic_base[tn].find(c); - if (it != d_generic_base[tn].end()) - { - return it->second; - } - TermDbSygus* tds = d_qe->getTermDatabaseSygus(); - Assert(tds->isRegistered(tn)); - Node g = tds->mkGeneric(dt, c); - Trace("csi-sol-debug") << "Generic is " << g << std::endl; - Node gr = Rewriter::rewrite(g); - Trace("csi-sol-debug") << "Generic rewritten is " << gr << std::endl; - d_generic_base[tn][c] = gr; - return gr; -} - -Node CegSingleInvSol::minimizeBuiltinTerm(Node n) -{ - Kind nk = n.getKind(); - if ((nk != EQUAL && nk != LEQ && nk != LT && nk != GEQ && nk != GT) - || !n[0].getType().isReal()) - { - return n; - } - NodeManager* nm = NodeManager::currentNM(); - bool changed = false; - std::vector mon[2]; - for (unsigned r = 0; r < 2; r++) - { - unsigned ro = r == 0 ? 1 : 0; - Node c; - Node nc; - if (n[r].getKind() == PLUS) - { - for (unsigned i = 0; i < n[r].getNumChildren(); i++) - { - if (ArithMSum::getMonomial(n[r][i], c, nc) - && c.getConst().isNegativeOne()) - { - mon[ro].push_back(nc); - changed = true; - } - else - { - if (!n[r][i].isConst() || !n[r][i].getConst().isZero()) - { - mon[r].push_back(n[r][i]); - } - } - } - } - else - { - if (ArithMSum::getMonomial(n[r], c, nc) - && c.getConst().isNegativeOne()) - { - mon[ro].push_back(nc); - changed = true; - } - else - { - if (!n[r].isConst() || !n[r].getConst().isZero()) - { - mon[r].push_back(n[r]); - } - } - } - } - if (changed) - { - Node nn[2]; - for (unsigned r = 0; r < 2; r++) - { - nn[r] = mon[r].size() == 0 - ? nm->mkConst(Rational(0)) - : (mon[r].size() == 1 ? mon[r][0] : nm->mkNode(PLUS, mon[r])); - } - return nm->mkNode(n.getKind(), nn[0], nn[1]); - } - return n; -} - -Kind CegSingleInvSol::getComparisonKind(TypeNode tn) -{ - if (tn.isInteger() || tn.isReal()) - { - return LT; - } - else if (tn.isBitVector()) - { - return BITVECTOR_ULT; - } - return UNDEFINED_KIND; -} - -Kind CegSingleInvSol::getPlusKind(TypeNode tn, bool is_neg) -{ - if (tn.isInteger() || tn.isReal()) - { - return is_neg ? MINUS : PLUS; - } - else if (tn.isBitVector()) - { - return is_neg ? BITVECTOR_SUB : BITVECTOR_PLUS; - } - return UNDEFINED_KIND; -} -} -} -} diff --git a/src/theory/quantifiers/sygus/ce_guided_single_inv_sol.h b/src/theory/quantifiers/sygus/ce_guided_single_inv_sol.h deleted file mode 100644 index 9aec30049..000000000 --- a/src/theory/quantifiers/sygus/ce_guided_single_inv_sol.h +++ /dev/null @@ -1,205 +0,0 @@ -/********************* */ -/*! \file ce_guided_single_inv_sol.h - ** \verbatim - ** Top contributors (to current version): - ** Andrew Reynolds, Mathias Preiner - ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2021 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 utility for reconstructing solutions for single invocation synthesis - ** conjectures - **/ - -#include "cvc4_private.h" - -#ifndef CVC4__THEORY__QUANTIFIERS__CE_GUIDED_SINGLE_INV_SOL_H -#define CVC4__THEORY__QUANTIFIERS__CE_GUIDED_SINGLE_INV_SOL_H - -#include -#include - -#include "context/cdhashmap.h" -#include "expr/dtype.h" -#include "expr/node.h" - -namespace CVC4 { -namespace theory { - -class QuantifiersEngine; - -namespace quantifiers { - -class CegSingleInv; - -/** CegSingleInvSol - * - * This function implements Figure 5 of "Counterexample-Guided Quantifier - * Instantiation for Synthesis in SMT", Reynolds et al CAV 2015. - * - */ -class CegSingleInvSol -{ - friend class CegSingleInv; - - private: - QuantifiersEngine * d_qe; - std::vector< Node > d_varList; - std::map< Node, int > d_dterm_size; - std::map< Node, int > d_dterm_ite_size; - - public: - CegSingleInvSol(QuantifiersEngine* qe); - /** reconstruct solution - * - * Returns (if possible) a node that is equivalent to sol those syntax - * matches the grammar corresponding to sygus datatype stn. - * The value reconstructed is set to 1 if we successfully return a node, - * otherwise it is set to -1. - * - * This method quickly tries to match sol to the grammar induced by stn. If - * this fails, we use enumerative techniques to try to repair the solution. - * The number of iterations for this enumeration is bounded by the argument - * enumLimit if it is positive, and unbounded otherwise. - */ - Node reconstructSolution(Node sol, - TypeNode stn, - int& reconstructed, - int enumLimit); - /** preregister conjecture - * - * q : the synthesis conjecture this class is for. - * This is used as a heuristic to find terms in the original conjecture which - * may be helpful for using during reconstruction. - */ - void preregisterConjecture(Node q); - - private: - int d_id_count; - int d_root_id; - std::map< int, Node > d_id_node; - std::map< int, TypeNode > d_id_type; - std::map< TypeNode, std::map< Node, int > > d_rcons_to_id; - std::map< TypeNode, std::map< Node, int > > d_rcons_to_status; - - std::map< int, std::map< Node, std::vector< int > > > d_reconstruct_op; - std::map< int, Node > d_reconstruct; - std::map< int, std::vector< int > > d_parents; - - std::map< int, std::vector< int > > d_eqc; - std::map< int, int > d_rep; - - //equivalent terms - std::map< Node, Node > d_eqt_rep; - std::map< Node, std::vector< Node > > d_eqt_eqc; - - //cache when reconstructing solutions - std::vector< int > d_tmp_fail; - // get reconstructed solution - Node getReconstructedSolution( int id, bool mod_eq = true ); - - // allocate node with type - int allocate( Node n, TypeNode stn ); - // term t with sygus type st, returns inducted templated form of t - int collectReconstructNodes( Node t, TypeNode stn, int& status ); - bool collectReconstructNodes(int pid, - std::vector& ts, - const DTypeConstructor& dtc, - std::vector& ids, - int& status); - bool getPathToRoot( int id ); - void setReconstructed( int id, Node n ); - //get equivalent terms to n with top symbol k - void getEquivalentTerms( Kind k, Node n, std::vector< Node >& equiv ); - //register equivalent terms - void registerEquivalentTerms( Node n ); - /** builtin to sygus const - * - * Returns a sygus term of type tn that encodes the builtin constant c. - * If the sygus datatype tn allows any constant, this may return a variable - * with the attribute SygusPrintProxyAttribute that associates it with c. - * - * rcons_depth limits the number of recursive calls when doing accelerated - * constant reconstruction (currently limited to 1000). Notice this is hacky: - * depending upon order of calls, constant rcons may succeed, e.g. 1001, 999 - * vs. 999, 1001. - */ - Node builtinToSygusConst(Node c, TypeNode tn, int rcons_depth = 0); - /** cache for the above function */ - std::map > d_builtin_const_to_sygus; - /** sorted list of constants, per type */ - std::map > d_const_list; - /** number of positive constants, per type */ - std::map d_const_list_pos; - /** list of constructor indices whose operators are identity functions */ - std::map > d_id_funcs; - /** initialize the above information for sygus type tn */ - void registerType(TypeNode tn); - /** get generic base - * - * This returns the builtin term that is the analog of an application of the - * c^th constructor of dt to fresh variables. - */ - Node getGenericBase(TypeNode tn, const DType& dt, int c); - /** cache for the above function */ - std::map > d_generic_base; - /** get match - * - * This function attempts to find a substitution for which p = n. If - * successful, this function returns a substitution in the form of s/new_s, - * where: - * s : substitution, where the domain are indices of terms in the sygus - * term database, and - * new_s : the members that were added to s on this call. - * Otherwise, this function returns false and s and new_s are unmodified. - */ - bool getMatch(Node p, - Node n, - std::map& s, - std::vector& new_s); - /** get match - * - * This function attempts to find a builtin term that is analog to a value - * of the sygus datatype st that is equivalent to n. If this function returns - * true, then it has found such a term. Then we set: - * index_found : updated to the constructor index of the sygus term whose - * analog to equivalent to n. - * args : builtin terms corresponding to the match, in order. - * Otherwise, this function returns false and index_found and args are - * unmodified. - * For example, for grammar: - * A -> 0 | 1 | x | +( A, A ) - * Given input ( 5 + (x+1) ) and A we would return true, where: - * index_found is set to 3 and args is set to { 5, x+1 }. - * - * index_exc : (if applicable) exclude a constructor index of st - * index_start : start index of constructors of st to try - */ - bool getMatch(Node n, - TypeNode st, - int& index_found, - std::vector& args, - int index_exc = -1, - int index_start = 0); - /** given a term, construct an equivalent smaller one that respects syntax */ - Node minimizeBuiltinTerm(Node n); - /** - * Return the kind of "is less than" for type tn, where tn is either Int or - * BV. - */ - static Kind getComparisonKind(TypeNode tn); - /** - * Return the kind of "plus" for type tn, or "minus" if is_neg is true, where - * tn is either Int or BV. - */ - static Kind getPlusKind(TypeNode tn, bool is_neg = false); -}; - - -} -} -} - -#endif diff --git a/src/theory/quantifiers/sygus/rcons_obligation_info.cpp b/src/theory/quantifiers/sygus/rcons_obligation_info.cpp new file mode 100644 index 000000000..25aac1e93 --- /dev/null +++ b/src/theory/quantifiers/sygus/rcons_obligation_info.cpp @@ -0,0 +1,100 @@ +/********************* */ +/*! \file rcons_obligation_info.cpp + ** \verbatim + ** Top contributors (to current version): + ** Abdalrhman Mohamed + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2021 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 Reconstruct Obligation Info class implementation + **/ + +#include "rcons_obligation_info.h" + +#include "expr/node_algorithm.h" +#include "theory/datatypes/sygus_datatype_utils.h" + +namespace CVC4 { +namespace theory { +namespace quantifiers { + +RConsObligationInfo::RConsObligationInfo(Node builtin) : d_builtin(builtin) {} + +Node RConsObligationInfo::getBuiltin() const { return d_builtin; } + +void RConsObligationInfo::addCandidateSolution(Node candSol) +{ + d_candSols.emplace(candSol); +} + +const std::unordered_set& +RConsObligationInfo::getCandidateSolutions() const +{ + return d_candSols; +} + +void RConsObligationInfo::addCandidateSolutionToWatchSet(Node candSol) +{ + d_watchSet.emplace(candSol); +} + +const std::unordered_set& +RConsObligationInfo::getWatchSet() const +{ + return d_watchSet; +} + +std::string RConsObligationInfo::obToString(Node k, + const RConsObligationInfo& obInfo) +{ + return "ob<" + obInfo.getBuiltin().toString() + ", " + k.getType().toString() + + ">"; +} + +void RConsObligationInfo::printCandSols( + const Node& root, + const std::unordered_map& + obInfo) +{ + std::unordered_set visited; + std::vector stack; + stack.push_back(root); + + Trace("sygus-rcons") << "\nEq classes: \n["; + + while (!stack.empty()) + { + const Node& k = stack.back(); + stack.pop_back(); + visited.emplace(k); + + Trace("sygus-rcons") << std::endl + << datatypes::utils::sygusToBuiltin(k) << " " + << obToString(k, obInfo.at(k)) << ":\n ["; + + for (const Node& j : obInfo.at(k).getCandidateSolutions()) + { + Trace("sygus-rcons") << datatypes::utils::sygusToBuiltin(j) << " "; + std::unordered_set subObs; + expr::getVariables(j, subObs); + for (const TNode& l : subObs) + { + if (visited.find(l) == visited.cend() + && obInfo.find(l) != obInfo.cend()) + { + stack.push_back(l); + } + } + } + Trace("sygus-rcons") << "]" << std::endl; + } + + Trace("sygus-rcons") << "]" << std::endl; +} + +} // namespace quantifiers +} // namespace theory +} // namespace CVC4 diff --git a/src/theory/quantifiers/sygus/rcons_obligation_info.h b/src/theory/quantifiers/sygus/rcons_obligation_info.h new file mode 100644 index 000000000..5ebddd794 --- /dev/null +++ b/src/theory/quantifiers/sygus/rcons_obligation_info.h @@ -0,0 +1,150 @@ +/********************* */ +/*! \file rcons_obligation_info.h + ** \verbatim + ** Top contributors (to current version): + ** Abdalrhman Mohamed + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2021 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 utility class for Sygus Reconstruct module + **/ + +#include "cvc4_private.h" + +#ifndef CVC4__THEORY__QUANTIFIERS__RCONS_OBLIGATION_INFO_H +#define CVC4__THEORY__QUANTIFIERS__RCONS_OBLIGATION_INFO_H + +#include "expr/node.h" + +namespace CVC4 { +namespace theory { +namespace quantifiers { + +/** + * A utility class for Sygus Reconstruct obligations. An obligation is a builtin + * term t and a SyGuS type T, and indicates that we are trying to build a term + * of type T whose builtin analog is equivalent to t. The main algorithm encodes + * each obligation (t, T) as a skolem k of type T to embed obligations in + * candidate solutions (see d_candSols below). It mainly operates over skolems + * and stores cooresponding builtin terms and other info in instances of this + * class. Notice that the SyGuS type T of an obligation is not stored in this + * class as it can be inferred from the type of the skolem k. + */ +class RConsObligationInfo +{ + public: + /** + * Constructor. Default value needed for maps. + * + * @param builtin builtin term to reconstruct + */ + explicit RConsObligationInfo(Node builtin = Node::null()); + + /** + * @return builtin term to reconstruct for this class' obligation + */ + Node getBuiltin() const; + + /** + * Add candidate solution to the set of candidate solutions for the + * corresponding obligation. + * + * @param candSol the candidate solution to add + */ + void addCandidateSolution(Node candSol); + + /** + * @return set of candidate solutions for this class' obligation + */ + const std::unordered_set& getCandidateSolutions() + const; + + /** + * Add candidate solution to the set of candidate solutions waiting for the + * corresponding obligation to be solved. + * + * @param candSol the candidate solution to add to watch set + */ + void addCandidateSolutionToWatchSet(Node candSol); + + /** + * @return set of candidate solutions waiting for this class' obligation + * to be solved + */ + const std::unordered_set& getWatchSet() const; + + /** + * Return a string representation of an obligation. + * + * @param k An obligation + * @param obInfo Obligation `k`'s info + * @return A string representation of `k` + */ + static std::string obToString(Node k, const RConsObligationInfo& obInfo); + + /** + * Print all reachable obligations and their candidate solutions from + * the `root` obligation and its candidate solutions. + * + * An obligation is reachable from the `root` obligation if it is the `root` + * obligation or is needed by one of the candidate solutions of other + * reachable obligations. + * + * For example, if we have: + * + * Obs = {c_z1, c_z2, c_z3, c_z4} // list of obligations in rcons algorithm + * CandSols = {c_z1 -> {(c_+ c_1 c_z2)}, c_z2 -> {(c_- c_z3)}, + * c_z3 -> {c_x}, c_z4 -> {}} + * root = c_z1 + * + * Then, the set of reachable obligations from `root` is {c_z1, c_z2, c_z3} + * + * \note requires enabling "sygus-rcons" trace + * + * @param root The root obligation to start from + * @param obInfo a map from obligations to their corresponding infos + */ + static void printCandSols( + const Node& root, + const std::unordered_map& + obInfo); + + private: + /** Builtin term for this class' obligation. + * + * To solve the obligation, this builtin term must be reconstructed in the + * specified grammar (sygus datatype type) of this class' obligation. + */ + Node d_builtin; + /** A set of candidate solutions to this class' obligation. + * + * Each candidate solution is a sygus datatype term containing skolem subterms + * (sub-obligations). By replacing all sub-obligations with their + * corresponding solutions, we get a term whose builtin analog rewrites to + * `d_builtin` and hence solves this obligation. For example, given: + * d_builtin = (+ x y) + * a possible set of candidate solutions would be: + * d_candSols = {(c_+ c_z1 c_z2), (c_+ c_x c_z2), (c_+ c_z1 c_y), + * (c_+ c_x c_y)} + * where c_z1 and c_z2 are skolems. Notice that `d_candSols` may contain a + * pure term that solves the obligation ((c_+ c_x c_y) in this example). + */ + std::unordered_set d_candSols; + /** A set of candidate solutions waiting for this class' obligation to + * be solved. + * + * In the example above, (c_+ c_z1 c_z2) and (c_+ c_x c_z2) are in + * the watch-set of c_z2. Similarly, (c_+ c_z1 c_z2) and (c_+ c_z1 c_y) are in + * the watch-set of c_z1. + */ + std::unordered_set d_watchSet; +}; + +} // namespace quantifiers +} // namespace theory +} // namespace CVC4 + +#endif // CVC4__THEORY__QUANTIFIERS__RCONS_OBLIGATION_INFO_H diff --git a/src/theory/quantifiers/sygus/rcons_type_info.cpp b/src/theory/quantifiers/sygus/rcons_type_info.cpp new file mode 100644 index 000000000..d24c4d25d --- /dev/null +++ b/src/theory/quantifiers/sygus/rcons_type_info.cpp @@ -0,0 +1,72 @@ +/********************* */ +/*! \file rcons_type_info.cpp + ** \verbatim + ** Top contributors (to current version): + ** Abdalrhman Mohamed + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2021 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 Reconstruct Type Info class implementation + **/ + +#include "theory/quantifiers/sygus/rcons_type_info.h" + +#include "theory/datatypes/sygus_datatype_utils.h" + +namespace CVC4 { +namespace theory { +namespace quantifiers { + +void RConsTypeInfo::initialize(TermDbSygus* tds, + SygusStatistics& s, + TypeNode stn, + const std::vector& builtinVars) +{ + NodeManager* nm = NodeManager::currentNM(); + + d_enumerator.reset(new SygusEnumerator(tds, nullptr, s, true)); + d_enumerator->initialize(nm->mkSkolem("sygus_rcons", stn)); + d_crd.reset(new CandidateRewriteDatabase(true, false, true, false)); + // since initial samples are not always useful for equivalence checks, set + // their number to 0 + d_sygusSampler.initialize(stn, builtinVars, 0); + d_crd->initialize(builtinVars, &d_sygusSampler); +} + +Node RConsTypeInfo::nextEnum() +{ + if (!d_enumerator->increment()) + { + Trace("sygus-rcons") << "no increment" << std::endl; + return Node::null(); + } + + Node sz = d_enumerator->getCurrent(); + + Trace("sygus-rcons") << (sz == Node::null() + ? sz + : datatypes::utils::sygusToBuiltin(sz)) + << std::endl; + + return sz; +} + +Node RConsTypeInfo::addTerm(Node n) +{ + std::stringstream out; + return d_crd->addTerm(n, false, out); +} + +void RConsTypeInfo::setBuiltinToOb(Node builtin, Node ob) +{ + d_ob[builtin] = ob; +} + +Node RConsTypeInfo::builtinToOb(Node builtin) { return d_ob[builtin]; } + +} // namespace quantifiers +} // namespace theory +} // namespace CVC4 diff --git a/src/theory/quantifiers/sygus/rcons_type_info.h b/src/theory/quantifiers/sygus/rcons_type_info.h new file mode 100644 index 000000000..432d07687 --- /dev/null +++ b/src/theory/quantifiers/sygus/rcons_type_info.h @@ -0,0 +1,102 @@ +/********************* */ +/*! \file rcons_type_info.h + ** \verbatim + ** Top contributors (to current version): + ** Abdalrhman Mohamed + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2021 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 utility class for Sygus Reconstruct module + **/ + +#include "cvc4_private.h" + +#ifndef CVC4__THEORY__QUANTIFIERS__RCONS_TYPE_INFO_H +#define CVC4__THEORY__QUANTIFIERS__RCONS_TYPE_INFO_H + +#include "theory/quantifiers/sygus/sygus_enumerator.h" + +namespace CVC4 { +namespace theory { +namespace quantifiers { + +/** + * A utility class for Sygus Reconstruct datatype types (grammar non-terminals). + * This class is mainly responsible for enumerating sygus datatype type terms + * and building sets of equivalent builtin terms for the rcons algorithm. + */ +class RConsTypeInfo +{ + public: + /** + * Initialize a sygus enumerator and a candidate rewrite database for this + * class' sygus datatype type. + * + * @param tds Database for sygus terms + * @param s Statistics managed for the synth engine + * @param stn The sygus datatype type encoding the syntax restrictions + * @param builtinVars A list containing the builtin analog of sygus variable + * list for the sygus datatype type + */ + void initialize(TermDbSygus* tds, + SygusStatistics& s, + TypeNode stn, + const std::vector& builtinVars); + + /** + * Returns the next enumerated term for the given sygus datatype type. + * + * @return The enumerated sygus term + */ + Node nextEnum(); + + /** + * Add a pure term to the candidate rewrite database. + * + * @param n The term to add to the database + * @return A previous term `eq_n` added to this class, such that `n` is + * equivalent to `eq_n`. If no previous term equivalent to `n` exists then the + * result is `n` itself + */ + Node addTerm(Node n); + + /** + * Set the obligation responsible for solving the given builtin term. + * + * @param builtin The builtin term + * @param ob The corresponding obligation + */ + void setBuiltinToOb(Node builtin, Node ob); + + /** + * Return the obligation responsible for solving the given builtin term. + * + * @param builtin The builtin term + * @return The corresponding obligation + */ + Node builtinToOb(Node builtin); + + private: + /** Sygus terms enumerator for this class' Sygus datatype type */ + std::unique_ptr d_enumerator; + /** Candidate rewrite database for this class' sygus datatype type */ + std::unique_ptr d_crd; + /** Sygus sampler needed for initializing the candidate rewrite database */ + SygusSampler d_sygusSampler; + /** A map from a builtin term to its obligation. + * + * Each sygus datatype type has its own version of this map because it is + * possible to have multiple obligations to reconstruct the same builtin term + * from different sygus datatype types. + */ + std::unordered_map d_ob; +}; + +} // namespace quantifiers +} // namespace theory +} // namespace CVC4 + +#endif // CVC4__THEORY__QUANTIFIERS__RCONS_TYPE_INFO_H diff --git a/src/theory/quantifiers/sygus/sygus_reconstruct.cpp b/src/theory/quantifiers/sygus/sygus_reconstruct.cpp new file mode 100644 index 000000000..bd0f7c4dd --- /dev/null +++ b/src/theory/quantifiers/sygus/sygus_reconstruct.cpp @@ -0,0 +1,491 @@ +/********************* */ +/*! \file sygus_reconstruct.cpp + ** \verbatim + ** Top contributors (to current version): + ** Abdalrhman Mohamed + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2021 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 implementation for reconstruct + **/ + +#include "theory/quantifiers/sygus/sygus_reconstruct.h" + +#include "expr/node_algorithm.h" +#include "smt/command.h" +#include "theory/datatypes/sygus_datatype_utils.h" +#include "theory/rewriter.h" + +using namespace CVC4::kind; + +namespace CVC4 { +namespace theory { +namespace quantifiers { + +SygusReconstruct::SygusReconstruct(TermDbSygus* tds, SygusStatistics& s) + : d_tds(tds), d_stats(s) +{ +} + +Node SygusReconstruct::reconstructSolution(Node sol, + TypeNode stn, + int8_t& reconstructed, + uint64_t enumLimit) +{ + Trace("sygus-rcons") << "SygusReconstruct::reconstructSolution: " << sol + << std::endl; + Trace("sygus-rcons") << "- target sygus type is " << stn << std::endl; + Trace("sygus-rcons") << "- enumeration limit is " << enumLimit << std::endl; + + // this method may get called multiple times with the same object. We need to + // reset the state to avoid conflicts + clear(); + + initialize(stn); + + NodeManager* nm = NodeManager::currentNM(); + + /** a set of obligations that are not yet satisfied for each sygus datatype */ + TypeObligationSetMap unsolvedObs; + + // paramaters sol and stn constitute the main obligation to satisfy + Node mainOb = nm->mkSkolem("sygus_rcons", stn); + + // add the main obligation to the set of obligations that are not yet + // satisfied + unsolvedObs[stn].emplace(mainOb); + d_obInfo.emplace(mainOb, RConsObligationInfo(sol)); + d_stnInfo[stn].setBuiltinToOb(sol, mainOb); + + // We need to add the main obligation to the crd in case it cannot be broken + // down by matching. By doing so, we can solve the obligation using + // enumeration and crd (if it is in the grammar) + d_stnInfo[stn].addTerm(sol); + + // the set of unique (up to rewriting) patterns/shapes in the grammar used by + // matching + std::unordered_map, TypeNodeHashFunction> pool; + + uint64_t count = 0; + + // algorithm + while (d_sol[mainOb].isNull() && count < enumLimit) + { + // enumeration phase + // a temporary set of new obligations cached for processing in the match + // phase + TypeObligationSetMap obsPrime; + for (const std::pair& pair : unsolvedObs) + { + // enumerate a new term + Trace("sygus-rcons") << "enum: " << stn << ": "; + Node sz = d_stnInfo[pair.first].nextEnum(); + if (sz.isNull()) + { + continue; + } + Node builtin = Rewriter::rewrite(datatypes::utils::sygusToBuiltin(sz)); + // if enumerated term does not contain free variables, then its + // corresponding obligation can be solved immediately + if (sz.isConst()) + { + Node rep = d_stnInfo[pair.first].addTerm(builtin); + Node k = d_stnInfo[pair.first].builtinToOb(rep); + // check if the enumerated term solves an obligation + if (k.isNull()) + { + // if not, create an "artifical" obligation whose solution would be + // the enumerated term + k = nm->mkSkolem("sygus_rcons", pair.first); + d_obInfo.emplace(k, RConsObligationInfo(builtin)); + d_stnInfo[pair.first].setBuiltinToOb(builtin, k); + } + // mark the obligation as solved + markSolved(k, sz); + // Since we added the term to the candidate rewrite database, there is + // no point in adding it to the pool too + continue; + } + // if there are no matches (all calls to notify return true)... + if (d_poolTrie.getMatches(builtin, this)) + { + // then, this is a new term and we should add it to pool + d_poolTrie.addTerm(builtin); + pool[pair.first].push_back(sz); + for (Node k : pair.second) + { + if (d_sol[k].isNull()) + { + Trace("sygus-rcons") + << "ob: " << RConsObligationInfo::obToString(k, d_obInfo[k]) + << std::endl; + // try to match obligation k with the enumerated term sz + TypeObligationSetMap temp = matchNewObs(k, sz); + // cache the new obligations for processing in the match phase + for (const std::pair& tempPair : + temp) + { + obsPrime[tempPair.first].insert(tempPair.second.cbegin(), + tempPair.second.cend()); + } + } + } + } + } + // match phase + while (!obsPrime.empty()) + { + // a temporary set of new obligations cached for later processing + TypeObligationSetMap obsDPrime; + for (const std::pair& pair : obsPrime) + { + for (const Node& k : pair.second) + { + unsolvedObs[pair.first].emplace(k); + if (d_sol[k].isNull()) + { + Trace("sygus-rcons") + << "ob: " << RConsObligationInfo::obToString(k, d_obInfo[k]) + << std::endl; + for (Node sz : pool[pair.first]) + { + // try to match each newly generated and cached obligation + // with patterns in pool + TypeObligationSetMap temp = matchNewObs(k, sz); + // cache the new obligations for later processing + for (const std::pair& tempPair : + temp) + { + obsDPrime[tempPair.first].insert(tempPair.second.cbegin(), + tempPair.second.cend()); + } + } + } + } + } + obsPrime = std::move(obsDPrime); + } + // remove solved obligations from unsolvedObs + removeSolvedObs(unsolvedObs); + ++count; + } + + if (Trace("sygus-rcons").isConnected()) + { + RConsObligationInfo::printCandSols(mainOb, d_obInfo); + printPool(pool); + } + + // if the main obligation is solved, return the solution + if (!d_sol[mainOb].isNull()) + { + reconstructed = 1; + // The algorithm mostly works with rewritten terms and may not notice that + // the original terms contain variables eliminated by the rewriter. For + // example, rewrite((ite true 0 z)) = 0. In such cases, we replace those + // variables with ground values. + return d_sol[mainOb].isConst() ? Node(d_sol[mainOb]) + : mkGround(d_sol[mainOb]); + } + + // we ran out of elements, return null + reconstructed = -1; + Warning() << CommandFailure( + "Cannot get synth function: reconstruction to syntax failed."); + return d_sol[mainOb]; +} + +TypeObligationSetMap SygusReconstruct::matchNewObs(Node k, Node sz) +{ + NodeManager* nm = NodeManager::currentNM(); + TypeObligationSetMap obsPrime; + + // obligations generated by match. Note that we might have already seen (and + // even solved) those obligations, hence the name "candidate obligations" + std::unordered_map candObs; + // the builtin terms corresponding to sygus variables in the grammar are bound + // variables. However, we want the `match` method to treat them as ground + // terms. So, we add redundant substitutions + candObs.insert(d_sygusVars.cbegin(), d_sygusVars.cend()); + + // try to match the obligation's builtin term with the pattern sz + if (expr::match(Rewriter::rewrite(datatypes::utils::sygusToBuiltin(sz)), + d_obInfo[k].getBuiltin(), + candObs)) + { + // the bound variables z generated by the enumerators are reused across + // enumerated terms, so we need to replace them with our own skolems + std::vector> subs; + Trace("sygus-rcons") << "-- ct: " << sz << std::endl; + // remove redundant substitutions + for (const std::pair& pair : d_sygusVars) + { + candObs.erase(pair.first); + } + // for each candidate obligation + for (const std::pair& candOb : candObs) + { + TypeNode stn = + datatypes::utils::builtinVarToSygus(candOb.first).getType(); + Node newVar; + // have we come across a similar obligation before? + Node rep = d_stnInfo[stn].addTerm(candOb.second); + if (!d_stnInfo[stn].builtinToOb(rep).isNull()) + { + // if so, use the original obligation + newVar = d_stnInfo[stn].builtinToOb(rep); + } + else + { + // otherwise, create a new obligation of the corresponding sygus type + newVar = nm->mkSkolem("sygus_rcons", stn); + d_obInfo.emplace(newVar, candOb.second); + d_stnInfo[stn].setBuiltinToOb(candOb.second, newVar); + // if the candidate obligation is a constant and the grammar allows + // random constants + if (candOb.second.isConst() + && k.getType().getDType().getSygusAllowConst()) + { + // then immediately solve the obligation + markSolved(newVar, d_tds->getProxyVariable(stn, candOb.second)); + } + else + { + // otherwise, add this candidate obligation to this list of + // obligations + obsPrime[stn].emplace(newVar); + } + } + subs.emplace_back(datatypes::utils::builtinVarToSygus(candOb.first), + newVar); + } + // replace original free vars in sz with new ones + if (!subs.empty()) + { + sz = sz.substitute(subs.cbegin(), subs.cend()); + } + // sz is solved if it has no sub-obligations or if all of them are solved + bool isSolved = true; + for (const std::pair& sub : subs) + { + if (d_sol[sub.second].isNull()) + { + isSolved = false; + d_subObs[sz].push_back(sub.second); + } + } + + if (isSolved) + { + Node s = sz.substitute(d_sol); + markSolved(k, s); + } + else + { + // add sz as a possible solution to obligation k + d_obInfo[k].addCandidateSolution(sz); + d_parentOb[sz] = k; + d_obInfo[d_subObs[sz].back()].addCandidateSolutionToWatchSet(sz); + } + } + + return obsPrime; +} + +void SygusReconstruct::markSolved(Node k, Node s) +{ + // return if obligation k is already solved + if (!d_sol[k].isNull()) + { + return; + } + + Trace("sygus-rcons") << "sol: " << s << std::endl; + Trace("sygus-rcons") << "builtin sol: " << datatypes::utils::sygusToBuiltin(s) + << std::endl; + + // First, mark `k` as solved + d_obInfo[k].addCandidateSolution(s); + d_sol[k] = s; + d_parentOb[s] = k; + + std::vector stack; + stack.push_back(k); + + while (!stack.empty()) + { + Node curr = stack.back(); + stack.pop_back(); + + // for each partial solution/parent of the now solved obligation `curr` + for (Node parent : d_obInfo[curr].getWatchSet()) + { + // remove `curr` and (possibly) other solved obligations from its list + // of children + while (!d_subObs[parent].empty() + && !d_sol[d_subObs[parent].back()].isNull()) + { + d_subObs[parent].pop_back(); + } + + // if the partial solution does not have any more children... + if (d_subObs[parent].empty()) + { + // then it is completely solved and can be used as a solution of its + // corresponding obligation + Node parentSol = parent.substitute(d_sol); + Node parentOb = d_parentOb[parent]; + // proceed only if parent obligation is not already solved + if (d_sol[parentOb].isNull()) + { + d_obInfo[parentOb].addCandidateSolution(parentSol); + d_sol[parentOb] = parentSol; + d_parentOb[parentSol] = parentOb; + // repeat the same process for the parent obligation + stack.push_back(parentOb); + } + } + else + { + // if it does have remaining children, add it to the watch list of one + // of them (picked arbitrarily) + d_obInfo[d_subObs[parent].back()].addCandidateSolutionToWatchSet( + parent); + } + } + } +} + +void SygusReconstruct::initialize(TypeNode stn) +{ + std::vector builtinVars; + + // Cache the sygus variables introduced by the problem (which we treat as + // ground terms when calling the `match` method) as opposed to the sygus + // variables introduced by the enumerators (which we treat as bound + // variables). + for (Node sv : stn.getDType().getSygusVarList()) + { + builtinVars.push_back(datatypes::utils::sygusToBuiltin(sv)); + d_sygusVars.emplace(datatypes::utils::sygusToBuiltin(sv), + datatypes::utils::sygusToBuiltin(sv)); + } + + SygusTypeInfo stnInfo; + stnInfo.initialize(d_tds, stn); + + // find the non-terminals of the grammar + std::vector sfTypes; + stnInfo.getSubfieldTypes(sfTypes); + + // initialize the enumerators and candidate rewrite databases. Notice here + // that we treat the sygus variables introduced by the problem as bound + // variables (needed for making sure that obligations are equal). This is fine + // as we will never add variables that were introduced by the enumerators to + // the database. + for (TypeNode tn : sfTypes) + { + d_stnInfo[tn].initialize(d_tds, d_stats, tn, builtinVars); + } +} + +void SygusReconstruct::removeSolvedObs(TypeObligationSetMap& unsolvedObs) +{ + for (std::pair& tempPair : unsolvedObs) + { + ObligationSet::iterator it = tempPair.second.begin(); + while (it != tempPair.second.end()) + { + if (d_sol[*it].isNull()) + { + ++it; + } + else + { + it = tempPair.second.erase(it); + } + } + } +} + +Node SygusReconstruct::mkGround(Node n) const +{ + // get the set of bound variables in n + std::unordered_set vars; + expr::getVariables(n, vars); + + std::unordered_map subs; + + // generate a ground value for each one of those variables + for (const TNode& var : vars) + { + subs.emplace(var, var.getType().mkGroundValue()); + } + + // substitute the variables with ground values + return n.substitute(subs); +} + +bool SygusReconstruct::notify(Node s, + Node n, + std::vector& vars, + std::vector& subs) +{ + for (size_t i = 0; i < vars.size(); ++i) + { + // We consider sygus variables as ground terms. So, if they are not equal to + // their substitution, then s is not matchable with n and we try the next + // term s. Example: If s = (+ z x) and n = (+ z y), then s is not matchable + // with n and we return true + if (d_sygusVars.find(vars[i]) != d_sygusVars.cend() && vars[i] != subs[i]) + { + return true; + } + } + // Note: false here means that we finally found an s that is matchable with n, + // so we should not add n to the pool + return false; +} + +void SygusReconstruct::clear() +{ + d_obInfo.clear(); + d_stnInfo.clear(); + d_sol.clear(); + d_subObs.clear(); + d_parentOb.clear(); + d_sygusVars.clear(); + d_poolTrie.clear(); +} + +void SygusReconstruct::printPool( + const std::unordered_map, TypeNodeHashFunction>& + pool) const +{ + Trace("sygus-rcons") << "\nPool:\n["; + + for (const std::pair>& pair : pool) + { + Trace("sygus-rcons") << std::endl << pair.first << ":\n[" << std::endl; + + for (const Node& sygusTerm : pair.second) + { + Trace("sygus-rcons") << " " + << Rewriter::rewrite( + datatypes::utils::sygusToBuiltin(sygusTerm)) + .toString() + << std::endl; + } + + Trace("sygus-rcons") << "]" << std::endl; + } + + Trace("sygus-rcons") << "]" << std::endl; +} + +} // namespace quantifiers +} // namespace theory +} // namespace CVC4 diff --git a/src/theory/quantifiers/sygus/sygus_reconstruct.h b/src/theory/quantifiers/sygus/sygus_reconstruct.h new file mode 100644 index 000000000..2d55c3f3d --- /dev/null +++ b/src/theory/quantifiers/sygus/sygus_reconstruct.h @@ -0,0 +1,312 @@ +/********************* */ +/*! \file sygus_reconstruct.h + ** \verbatim + ** Top contributors (to current version): + ** Abdalrhman Mohamed + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2021 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 utility for reconstructing terms to match a grammar + **/ + +#include "cvc4_private.h" + +#ifndef CVC4__THEORY__QUANTIFIERS__SYGUS_RECONSTRUCT_H +#define CVC4__THEORY__QUANTIFIERS__SYGUS_RECONSTRUCT_H + +#include +#include + +#include "theory/quantifiers/sygus/rcons_obligation_info.h" +#include "theory/quantifiers/sygus/rcons_type_info.h" + +namespace CVC4 { +namespace theory { +namespace quantifiers { + +using ObligationSet = std::unordered_set; +using TypeObligationSetMap = + std::unordered_map; + +/** SygusReconstruct + * + * This class implements an algorithm for reconstructing a given term such that + * the reconstructed term is equivalent to the original term and its syntax + * matches a specified grammar. + * + * Goal: find a term g in sygus type T_0 that is equivalent to builtin term t_0. + * + * rcons(t_0, T_0) returns g + * { + * Obs: A map from sygus types T to a set of triples to reconstruct into T, + * where each triple is of the form (k, t, s), where k is a skolem of + * type T, t is a builtin term of the type encoded by T, and s is a + * possibly null sygus term of type T representing the solution. + * + * Sol: A map from skolems k to solutions s in the triples (k, t, s). That is, + * Sol[k] = s. + * + * CandSols : A map from a skolem k to a set of possible solutions for its + * corresponding obligation. Whenever there is a successful match, + * it is added to this set. + * + * Pool : A map from a sygus type T to a set of enumerated terms in T. + * The terms in this pool are patterns whose builtin analogs are used + * for matching against the terms to reconstruct t in (k, t, s). + * + * let k_0 be a fresh skolem of sygus type T_0 + * Obs[T_0] += (k_0, t_0, null) + * + * while Sol[k_0] == null + * Obs' = {} // map from T to sets of triples pending addition to Obs + * // enumeration phase + * for each subfield type T of T_0 + * // enumerated terms may contain variables z ranging over all terms of + * // their type (subfield types of T_0) + * s[z] = nextEnum(T) + * builtin = rewrite(toBuiltIn(s[z])) + * if (s[z] is ground) + * // let X be the theory the solver is invoked with + * find (k, t, s) in Obs[T] s.t. |=_X t = builtin + * if no such triple exists + * let k be a new variable of type : T + * Obs[T] += (k, builtin, null) + * markSolved(k, s[z]) + * else if no s' in Pool[T] and matcher sigma s.t. + * rewrite(toBuiltIn(s')) * sigma = builtin + * Pool[T] += s[z] + * for each (k, t, null) in Obs[T] + * Obs' += matchNewObs(k, s[z]) + * // match phase + * while Obs' != {} + * Obs'' = {} + * for each (k, t, null) in Obs' // s = null for all triples in Obs' + * Obs[T] += (k, t, null) + * for each s[z] in Pool[T] + * Obs'' += matchNewObs(k, s[z]) + * Obs' = Obs'' + * g = Sol[k_0] + * instantiate free variables of g with arbitrary sygus datatype values + * } + * + * matchNewObs(k, s[z]) returns Obs' + * { + * u = rewrite(toBuiltIn(s[z])) + * if match(u, t) == {toBuiltin(z) -> t'} + * // let X be the theory the solver is invoked with + * if forall t' exists (k'', t'', s'') in Obs[T] s.t. |=_X t'' = t' + * markSolved(k, s{z -> s''}) + * else + * let k' be a new variable of type : typeOf(z) + * CandSol[k] += s{z -> k'} + * Obs'[typeOf(z)] += (k', t', null) + * } + * + * markSolved(k, s) + * { + * if Sol[k] != null + * return + * Sol[k] = s + * CandSols[k] += s + * Stack = {k} + * while Stack != {} + * k' = pop(Stack) + * for all k'' in CandSols keys + * for all s'[k'] in CandSols[k''] + * s'{k' -> Sol[k']} + * if s' does not contain free variables in Obs + * Sol[k''] = s' + * push(Stack, k'') + * } + */ +class SygusReconstruct : public expr::NotifyMatch +{ + public: + /** + * Constructor. + * + * @param tds Database for sygus terms + * @param s Statistics managed for the synth engine + */ + SygusReconstruct(TermDbSygus* tds, SygusStatistics& s); + + /** Reconstruct solution. + * + * Return (if possible) a sygus encoding of a node that is equivalent to sol + * and whose syntax matches the grammar corresponding to sygus datatype stn. + * + * For example, given: + * sol = (* 2 x) + * stn = A sygus datatype encoding the grammar + * Start -> (c_PLUS Start Start) | c_x | c_0 | c_1 + * This method may return (c_PLUS c_x c_x) and set reconstructed to 1. + * + * @param sol The target term + * @param stn The sygus datatype type encoding the syntax restrictions + * @param reconstructed The flag to update, set to 1 if we successfully return + * a node, otherwise it is set to -1 + * @param enumLimit A value to limit the effort spent by this class (roughly + * equal to the number of intermediate terms to try) + * @return The reconstructed sygus term + */ + Node reconstructSolution(Node sol, + TypeNode stn, + int8_t& reconstructed, + uint64_t enumLimit); + + private: + /** Match obligation `k`'s builtin term with pattern `sz`. + * + * This function matches the builtin term to reconstruct for obligation `k` + * with the builtin analog of the pattern `sz`. If the match succeeds, `sz` is + * added to the set of candidate solutions for `k` and a set of new + * sub-obligations to satisfy is returned. If there are no new sub-obligations + * to satisfy, then `sz` is considered a solution to obligation `k` and + * `matchNewObs(k, sz)` is called. For example, given: + * + * Obs[typeOf(c_z1)] = {(c_z1, (+ 1 1), null)} + * Pool[typeOf(c_z1)] = {(c_+ c_z2 c_z3)} + * CandSols = {} + * + * Then calling `matchNewObs(c_z1, (c_+ c_z2 c_z3))` will result in: + * + * Obs[typeOf(c_z1)] = {(c_z1, (+ 1 1), null), (c_z4, 1, null)} + * Pool[typeOf(c_z1)] = {(c_+ c_z2 c_z3)} + * CandSols = {c_z1 -> {(c_+ c_z4 c_z4)}} + * + * and will return `{typeOf(c_z4) -> {c_z4}}`. + * + * Notice that `c_z2` and `c_z3` are not returned as new sub-obligations. + * Instead, `(c_+ c_z2 c_z3)` is instantiated with a new skolem `c_z4`, which + * is then added to the set of obligations. This is done to allow the reuse of + * patterns in `Pool`. Also, notice that only one new skolem/sub-obligation is + * generated. That's because the builtin analogs of `c_z2` and `c_z3` match + * with the same builtin term `1`. + * + * @param k free var whose builtin term we need to match + * @param sz a pattern to match `ob`s builtin term with + * @return a set of new obligations to satisfy if the match succeeds + */ + TypeObligationSetMap matchNewObs(Node k, Node sz); + + /** mark obligation `k` as solved. + * + * This function first marks `s` as the complete/constant solution for + * `ob`. Then it substitutes all instances of `ob` in partial solutions to + * other obligations with `s`. The function repeats those two steps for each + * partial solution that gets completed because of the second step. For + * example, given: + * + * CandSols = { + * mainOb -> {(+ z1 1)}, + * z1 -> {(* z2 x)}, + * z2 -> {2} + * } + * Sol = {z2 -> 2} + * + * Then calling `markSolved(z2, 2)` will result in: + * + * CandSols = { + * mainOb -> {(+ z1 1), (+ (* 2 x) 1)}, + * z1 -> {(* z2 x), (* 2 x)}, + * z2 -> {2} + * } + * Sol = {mainOb -> (+ (* 2 x) 1), z1 -> (* 2 x), z2 -> 2} + * + * Note: example uses builtin terms instead of sygus terms for simplicity. + * + * @param ob free var to mark as solved and substitute + * @param sol constant solution to `ob` + */ + void markSolved(Node k, Node s); + + /** + * Initialize a sygus enumerator and a candidate rewrite database for each + * sygus datatype type. + * + * @param stn The sygus datatype type encoding the syntax restrictions + */ + void initialize(TypeNode stn); + + /** + * Remove solved obligations from the given set of obligations. + * + * @param unsolvedObs A set of obligations containing solved ones + */ + void removeSolvedObs(TypeObligationSetMap& obs); + + /** + * Replace all variables in `n` with ground values. Before, calling `match`, + * `matchNewObs` rewrites the builtin analog of `n` which contains variables. + * The rewritten term, however, may contain fewer variables: + * + * rewrite((ite true z1 z2)) = z1 // n = (c_ite c_true c_z1 c_z2) + * + * In such cases, `matchNewObs` replaces the remaining variables (`c_z1`) with + * obligations and ignores the eliminated ones (`c_z2`). Since the values of + * the eliminated variables do not matter, they are replaced with some ground + * values by calling this method. + * + * @param n A term containing variables + * @return `n` with all vars in `n` replaced with ground values + */ + Node mkGround(Node n) const; + + /** + * A notification that s is equal to n * { vars -> subs }. This function + * should return false if we do not wish to be notified of further matches. + */ + bool notify(Node s, + Node n, + std::vector& vars, + std::vector& subs) override; + + /** + * Reset the state of this SygusReconstruct object. + */ + void clear(); + + /** + * Print the pool of patterns/shape used in the matching phase. + * + * \note requires enabling "sygus-rcons" trace + * + * @param pool a pool of patterns/shapes to print + */ + void printPool(const std::unordered_map, + TypeNodeHashFunction>& pool) const; + + /** pointer to the sygus term database */ + TermDbSygus* d_tds; + /** reference to the statistics of parent */ + SygusStatistics& d_stats; + + /** a map from an obligation to its reconstruction info */ + std::unordered_map d_obInfo; + /** a map from a sygus datatype type to its reconstruction info */ + std::unordered_map d_stnInfo; + + /** a map from an obligation to its sygus solution (if it exists) */ + std::unordered_map d_sol; + + /** a map from a candidate solution to its sub-obligations */ + std::unordered_map, NodeHashFunction> d_subObs; + /** a map from a candidate solution to its parent obligation */ + std::unordered_map d_parentOb; + + /** a cache of sygus variables treated as ground terms by matching */ + std::unordered_map d_sygusVars; + + /** A trie for filtering out redundant terms from the paterns pool */ + expr::MatchTrie d_poolTrie; +}; + +} // namespace quantifiers +} // namespace theory +} // namespace CVC4 + +#endif // CVC4__THEORY__QUANTIFIERS__SYGUS_RECONSTRUCT_H diff --git a/src/theory/quantifiers/sygus/synth_conjecture.cpp b/src/theory/quantifiers/sygus/synth_conjecture.cpp index 3a9864ea9..831216445 100644 --- a/src/theory/quantifiers/sygus/synth_conjecture.cpp +++ b/src/theory/quantifiers/sygus/synth_conjecture.cpp @@ -57,7 +57,7 @@ SynthConjecture::SynthConjecture(QuantifiersEngine* qe, d_stats(s), d_tds(qe->getTermDatabaseSygus()), d_hasSolution(false), - d_ceg_si(new CegSingleInv(qe)), + d_ceg_si(new CegSingleInv(qe, s)), d_templInfer(new SygusTemplateInfer), d_ceg_proc(new SynthConjectureProcess(qe)), d_ceg_gc(new CegGrammarConstructor(d_tds, this)), @@ -1037,7 +1037,7 @@ void SynthConjecture::printSynthSolution(std::ostream& out) Trace("cegqi-sol-debug") << "Printing synth solution..." << std::endl; Assert(d_quant[0].getNumChildren() == d_embed_quant[0].getNumChildren()); std::vector sols; - std::vector statuses; + std::vector statuses; if (!getSynthSolutionsInternal(sols, statuses)) { return; @@ -1049,7 +1049,7 @@ void SynthConjecture::printSynthSolution(std::ostream& out) if (!sol.isNull()) { Node prog = d_embed_quant[0][i]; - int status = statuses[i]; + int8_t status = statuses[i]; TypeNode tn = prog.getType(); const DType& dt = tn.getDType(); std::stringstream ss; @@ -1161,7 +1161,7 @@ bool SynthConjecture::getSynthSolutions( { NodeManager* nm = NodeManager::currentNM(); std::vector sols; - std::vector statuses; + std::vector statuses; Trace("cegqi-debug") << "getSynthSolutions..." << std::endl; if (!getSynthSolutionsInternal(sols, statuses)) { @@ -1173,7 +1173,7 @@ bool SynthConjecture::getSynthSolutions( for (unsigned i = 0, size = d_embed_quant[0].getNumChildren(); i < size; i++) { Node sol = sols[i]; - int status = statuses[i]; + int8_t status = statuses[i]; Trace("cegqi-debug") << "...got " << i << ": " << sol << ", status=" << status << std::endl; // get the builtin solution @@ -1220,7 +1220,7 @@ void SynthConjecture::recordSolution(std::vector& vs) } bool SynthConjecture::getSynthSolutionsInternal(std::vector& sols, - std::vector& statuses) + std::vector& statuses) { if (!d_hasSolution) { @@ -1234,7 +1234,7 @@ bool SynthConjecture::getSynthSolutionsInternal(std::vector& sols, Assert(tn.isDatatype()); // get the solution Node sol; - int status = -1; + int8_t status = -1; if (isSingleInvocation()) { Assert(d_ceg_si != NULL); diff --git a/src/theory/quantifiers/sygus/synth_conjecture.h b/src/theory/quantifiers/sygus/synth_conjecture.h index 27c565795..1b9f656bd 100644 --- a/src/theory/quantifiers/sygus/synth_conjecture.h +++ b/src/theory/quantifiers/sygus/synth_conjecture.h @@ -199,6 +199,9 @@ class SynthConjecture */ bool checkSideCondition(const std::vector& cvals) const; + /** get a reference to the statistics of parent */ + SygusStatistics& getSygusStatistics() { return d_stats; }; + private: /** reference to quantifier engine */ QuantifiersEngine* d_qe; @@ -387,7 +390,7 @@ class SynthConjecture * the sygus datatype constructor corresponding to variable x. */ bool getSynthSolutionsInternal(std::vector& sols, - std::vector& status); + std::vector& status); //-------------------------------- sygus stream /** * Prints the current synthesis solution to the output stream indicated by diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt index 6ae77b38b..2aa8861fd 100644 --- a/test/regress/CMakeLists.txt +++ b/test/regress/CMakeLists.txt @@ -1152,9 +1152,7 @@ set(regress_0_tests regress0/strings/unicode-esc.smt2 regress0/strings/unsound-0908.smt2 regress0/strings/unsound-repl-rewrite.smt2 - regress0/sygus/aig-si.sy regress0/sygus/array-grammar-select.sy - regress0/sygus/c100.sy regress0/sygus/ccp16.lus.sy regress0/sygus/cegqi-si-string-triv-2fun.sy regress0/sygus/cegqi-si-string-triv.sy @@ -1176,7 +1174,6 @@ set(regress_0_tests regress0/sygus/no-logic.sy regress0/sygus/no-syntax-test-bool.sy regress0/sygus/no-syntax-test.sy - regress0/sygus/parity-AIG-d0.sy regress0/sygus/parse-bv-let.sy regress0/sygus/pbe-pred-contra.sy regress0/sygus/pLTL-sygus-syntax-err.sy @@ -2207,6 +2204,12 @@ set(regress_1_tests regress1/sygus/max.sy regress1/sygus/max2-bv.sy regress1/sygus/multi-fun-polynomial2.sy + regress1/sygus/complex-no-rewrite.sy + regress1/sygus/complex-rewrite-in-db.sy + regress1/sygus/no-var-in-sol.sy + regress1/sygus/simple-no-rewrite.sy + regress1/sygus/simple-rewrite-in-db.sy + regress1/sygus/simple-rewrite-not-in-db.sy regress1/sygus/nflat-fwd-3.sy regress1/sygus/nflat-fwd.sy regress1/sygus/nia-max-square-ns.sy @@ -2215,7 +2218,6 @@ set(regress_1_tests regress1/sygus/no-mention.sy regress1/sygus/once_2.sy regress1/sygus/only-const-grammar.sy - regress1/sygus/parity-si-rcons.sy regress1/sygus/pbe_multi.sy regress1/sygus/phone-1-long.sy regress1/sygus/planning-unif.sy @@ -2556,10 +2558,19 @@ set(regression_disabled_tests regress1/sygus/interpol_from_pono_3.smt2 regress1/sygus/interpol_dt.smt2 regress1/sygus/inv_gen_fig8.sy - # rely on heuristic solution reconstruction TODO #3146 revisit + # new reconstruct algorithm is slow at reconstructing random constants (see wishue #82) + regress0/sygus/c100.sy + # For the six regressions below, solution terms require rewrites not in + # database and are too big to enumerate + regress0/sygus/aig-si.sy + regress0/sygus/parity-AIG-d0.sy regress1/sygus/array_search_2.sy regress1/sygus/array_sum_2_5.sy regress1/sygus/crcy-si-rcons.sy + regress1/sygus/parity-si-rcons.sy + # should print a better error message to indicate that a term is not in the + # provided grammar + regress1/sygus/simple-not-in-grammar.sy # previously sygus inference did not apply, now (correctly) times out regress1/sygus/issue3498.smt2 regress2/arith/miplib-opt1217--27.smt2 diff --git a/test/regress/regress1/sygus/array_search_2.sy b/test/regress/regress1/sygus/array_search_2.sy index b519c570f..c2404a12c 100644 --- a/test/regress/regress1/sygus/array_search_2.sy +++ b/test/regress/regress1/sygus/array_search_2.sy @@ -1,6 +1,6 @@ ; REQUIRES: proof ; EXPECT: unsat -; COMMAND-LINE: --lang=sygus2 --sygus-si=all --sygus-out=status --sygus-si-sol-min-core --proof +; COMMAND-LINE: --lang=sygus2 --sygus-si=all --sygus-out=status (set-logic LIA) (synth-fun findIdx ((y1 Int) (y2 Int) (k1 Int)) Int ((Start Int) (BoolExpr Bool)) ((Start Int ( 0 1 2 y1 y2 k1 (ite BoolExpr Start Start))) (BoolExpr Bool ((< Start Start) (<= Start Start) (> Start Start) (>= Start Start))))) (declare-var x1 Int) diff --git a/test/regress/regress1/sygus/complex-no-rewrite.sy b/test/regress/regress1/sygus/complex-no-rewrite.sy new file mode 100644 index 000000000..5a2d38cb8 --- /dev/null +++ b/test/regress/regress1/sygus/complex-no-rewrite.sy @@ -0,0 +1,21 @@ +; COMMAND-LINE: --sygus-si=all --sygus-out=status +; EXPECT: unsat + +(set-logic LIA) + +(synth-fun f ((x Int) (y Int)) Int + ((Start Int) (StartBool Bool)) + ((Start Int (0 1 x y + (+ Start Start) + (- Start Start) + (ite StartBool Start Start))) + (StartBool Bool ((and StartBool StartBool) + (not StartBool) + (<= Start Start))))) + +(declare-var x Int) +(declare-var y Int) + +(constraint (= (f x y) (ite (<= 1 x) (- 0 y) (+ x y)))) + +(check-synth) diff --git a/test/regress/regress1/sygus/complex-rewrite-in-db.sy b/test/regress/regress1/sygus/complex-rewrite-in-db.sy new file mode 100644 index 000000000..e3e017cec --- /dev/null +++ b/test/regress/regress1/sygus/complex-rewrite-in-db.sy @@ -0,0 +1,21 @@ +; COMMAND-LINE: --sygus-si=all --sygus-out=status +; EXPECT: unsat + +(set-logic LIA) + +(synth-fun f ((x Int) (y Int)) Int + ((Start Int) (StartBool Bool)) + ((Start Int (0 1 x y + (+ Start Start) + (- Start Start) + (ite StartBool Start Start))) + (StartBool Bool ((and StartBool StartBool) + (not StartBool) + (<= Start Start))))) + +(declare-var x Int) +(declare-var y Int) + +(constraint (= (f x y) (ite (<= (+ y 3) x) x (+ x y)))) + +(check-synth) diff --git a/test/regress/regress1/sygus/no-var-in-sol.sy b/test/regress/regress1/sygus/no-var-in-sol.sy new file mode 100644 index 000000000..333e29d6e --- /dev/null +++ b/test/regress/regress1/sygus/no-var-in-sol.sy @@ -0,0 +1,24 @@ +; COMMAND-LINE: --sygus-si=all --dag-thresh=0 +; EXPECT: unsat +; EXPECT: (define-fun f1 ((x Bool) (y Bool)) Bool (ite true true false)) +; EXPECT: (define-fun f2 ((x Bool) (y Bool)) Bool (ite x (ite y false (not false)) (not (ite false false (not false))))) + +; Test ensures that the solution does not contain a random variable + +(set-logic UF) + +(synth-fun f1 ((x Bool) (y Bool)) Bool + ((Start Bool)) + ((Start Bool (false (ite true true Start))))) + +(synth-fun f2 ((x Bool) (y Bool)) Bool + ((Start Bool)) + ((Start Bool (false x y (ite Start Start (not Start)))))) + +(declare-var x Bool) +(declare-var y Bool) + +(constraint (= (f1 x y) true)) +(constraint (= (f2 x y) (not (ite x y true)))) + +(check-synth) diff --git a/test/regress/regress1/sygus/simple-no-rewrite.sy b/test/regress/regress1/sygus/simple-no-rewrite.sy new file mode 100644 index 000000000..68e8a3a48 --- /dev/null +++ b/test/regress/regress1/sygus/simple-no-rewrite.sy @@ -0,0 +1,15 @@ +; COMMAND-LINE: --sygus-si=all --sygus-out=status +; EXPECT: unsat + +(set-logic UF) + +(synth-fun f ((x Bool) (y Bool)) Bool + ((Start Bool)) + ((Start Bool (true false x y (and Start Start) (or Start Start))))) + +(declare-var x Bool) +(declare-var y Bool) + +(constraint (= (f x y) (and x y))) + +(check-synth) diff --git a/test/regress/regress1/sygus/simple-not-in-grammar.sy b/test/regress/regress1/sygus/simple-not-in-grammar.sy new file mode 100644 index 000000000..f9f6354f5 --- /dev/null +++ b/test/regress/regress1/sygus/simple-not-in-grammar.sy @@ -0,0 +1,12 @@ +; COMMAND-LINE: --sygus-si=all --sygus-out=status +; EXPECT: unsat + +(set-logic UF) + +(synth-fun f () Bool + ((Start Bool)) + ((Start Bool (false)))) + +(constraint (= f true)) + +(check-synth) diff --git a/test/regress/regress1/sygus/simple-rewrite-in-db.sy b/test/regress/regress1/sygus/simple-rewrite-in-db.sy new file mode 100644 index 000000000..46d3b59b0 --- /dev/null +++ b/test/regress/regress1/sygus/simple-rewrite-in-db.sy @@ -0,0 +1,15 @@ +; COMMAND-LINE: --sygus-si=all --sygus-out=status +; EXPECT: unsat + +(set-logic UF) + +(synth-fun f ((x Bool) (y Bool)) Bool + ((Start Bool)) + ((Start Bool (true false x y (not Start) (= Start Start))))) + +(declare-var x Bool) +(declare-var y Bool) + +(constraint (= (f x y) (xor x y))) + +(check-synth) diff --git a/test/regress/regress1/sygus/simple-rewrite-not-in-db.sy b/test/regress/regress1/sygus/simple-rewrite-not-in-db.sy new file mode 100644 index 000000000..04d35fa71 --- /dev/null +++ b/test/regress/regress1/sygus/simple-rewrite-not-in-db.sy @@ -0,0 +1,16 @@ +; COMMAND-LINE: --sygus-si=all --sygus-si-rcons-limit=10000 --sygus-out=status +; EXPECT: unsat + +(set-logic UF) + +(synth-fun f ((x Bool) (y Bool)) Bool + ((Start Bool)) + ((Start Bool (true false x y (not Start) (and Start Start) (or Start Start))))) + +(declare-var x Bool) +(declare-var y Bool) + +(constraint (= (f x y) (= x y))) +; (or (and x y) (not (or x y))) + +(check-synth) -- 2.30.2