This PR replaces the old algorithm for reconstructing sygus terms with a new "proper" implementation.
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
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
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
Node substitute(Iterator substitutionsBegin,
Iterator substitutionsEnd) const;
+ /**
+ * Simultaneous substitution of Nodes in cache.
+ */
+ Node substitute(
+ std::unordered_map<TNode, TNode, TNodeHashFunction>& cache) const;
+
/**
* Returns the kind of this node.
* @return the kind
return substitute(substitutionsBegin, substitutionsEnd, cache);
}
+template <bool ref_count>
+inline Node NodeTemplate<ref_count>::substitute(
+ std::unordered_map<TNode, TNode, TNodeHashFunction>& 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 <bool ref_count>
template <class Iterator>
Node
bool filterPairs = true);
~CandidateRewriteDatabase() {}
/** Initialize this class */
- void initialize(const std::vector<Node>& var,
- SygusSampler* ss = nullptr) override;
+ void initialize(const std::vector<Node>& var, SygusSampler* ss) override;
/** Initialize this class
*
* Serves the same purpose as the above function, but we will be using
void initializeSygus(const std::vector<Node>& vars,
QuantifiersEngine* qe,
Node f,
- SygusSampler* ss = nullptr);
+ SygusSampler* ss);
/** add term
*
* Notifies this class that the solution sol was enumerated. This may
#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"
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),
}
Node CegSingleInv::getSolution(size_t sol_index,
TypeNode stn,
- int& reconstructed,
+ int8_t& reconstructed,
bool rconsSygus)
{
Assert(sol_index < d_quant[0].getNumChildren());
// 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<Node> vars;
+ std::vector<Node> 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)
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
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)
{
{
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);
#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
QuantifiersEngine* d_qe;
// single invocation inference utility
SingleInvocationPartition* d_sip;
- // solution reconstruction
- CegSingleInvSol* d_sol;
+ /** solution reconstruction */
+ std::unique_ptr<SygusReconstruct> d_srcons;
// list of skolems for each argument of programs
std::vector<Node> d_single_inv_arg_sk;
Node d_single_inv;
public:
- CegSingleInv(QuantifiersEngine* qe);
+ CegSingleInv(QuantifiersEngine* qe, SygusStatistics& s);
~CegSingleInv();
// get simplified conjecture
*/
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 */
+++ /dev/null
-/********************* */
-/*! \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<bool>();
-}
-
-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<n[0].getNumChildren(); i++ ){
- evars.push_back( n[0][i] );
- }
- n = n[1].substitute( evars.begin(), evars.end(), d_varList.begin(), d_varList.end() );
- }else{
- Trace("csi-sol") << "Not the same number of variables, return." << std::endl;
- return;
- }
- }
- Trace("csi-sol") << "Preregister node for solution reconstruction : " << n << std::endl;
- registerEquivalentTerms( n );
-}
-
-Node CegSingleInvSol::reconstructSolution(Node sol,
- TypeNode stn,
- int& reconstructed,
- int enumLimit)
-{
- Trace("csi-rcons") << "Solution (pre-reconstruction) is : " << sol << std::endl;
- int status;
- d_root_id = collectReconstructNodes( sol, stn, status );
- if( status==0 ){
- Node ret = getReconstructedSolution( d_root_id );
- Trace("csi-rcons") << "Sygus solution is : " << ret << std::endl;
- Assert(!ret.isNull());
- reconstructed = 1;
- return ret;
- }
- if (Trace.isOn("csi-rcons"))
- {
- for (std::map<TypeNode, std::map<Node, int> >::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<Node, int>::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<Node, int>::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<to_erase.size(); i++ ){
- active.erase( to_erase[i] );
- }
- index++;
- if( index%100==0 ){
- Trace("csi-rcons-stats") << "Tried " << index << " for each type." << std::endl;
- }
- } while (!active.empty() && (enumLimit < 0 || index < enumLimit));
- }
-
- // we ran out of elements, return null
- reconstructed = -1;
- Warning() << CommandFailure(
- "Cannot get synth function: reconstruction to syntax failed.");
- // could return sol here, however, we choose to fail by returning null, since
- // it indicates a failure.
- return Node::null();
-}
-
-int CegSingleInvSol::collectReconstructNodes(Node t, TypeNode stn, int& status)
-{
- std::map< Node, int >::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; i<min_t.getNumChildren(); i++ ){
- rem_children.push_back( min_t[i] );
- }
- Node t2 = NodeManager::currentNM()->mkNode( 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<min_t.getNumChildren(); i++ ){
- tchildren.push_back( min_t[i] );
- }
- }
- //recurse on the children
- if( tchildren.size()==dt[karg].getNumArgs() ){
- Trace("csi-rcons-debug") << "Type for " << id << " has kind " << min_t.getKind() << ", recurse." << std::endl;
- status = 0;
- Node cons = dt[karg].getConstructor();
- if( !collectReconstructNodes( id, tchildren, dt[karg], d_reconstruct_op[id][cons], status ) ){
- Trace("csi-rcons-debug") << "...failure for " << id << " " << dt[karg].getName() << std::endl;
- d_reconstruct_op[id].erase( cons );
- status = 1;
- }
- }else{
- Trace("csi-rcons-debug") << "Type for " << id << " has kind " << min_t.getKind() << ", but argument # mismatch." << std::endl;
- }
- }
- if( status!=0 ){
- //try constant reconstruction
- if( min_t.isConst() ){
- Trace("csi-rcons-debug") << "...try constant reconstruction." << std::endl;
- Node min_t_c = builtinToSygusConst(min_t, stn);
- if( !min_t_c.isNull() ){
- Trace("csi-rcons-debug") << " constant reconstruction success for " << id << ", result = " << min_t_c << std::endl;
- d_reconstruct[id] = min_t_c;
- status = 0;
- }
- }
- if( status!=0 ){
- //try identity functions
- for (unsigned ii : d_id_funcs[stn])
- {
- Assert(dt[ii].getNumArgs() == 1);
- //try to directly reconstruct from single argument
- std::vector< Node > tchildren;
- tchildren.push_back( min_t );
- TypeNode stnc = dt[ii][0].getRangeType();
- Trace("csi-rcons-debug") << "...try identity function " << dt[ii].getSygusOp() << ", child type is " << stnc << std::endl;
- status = 0;
- Node cons = dt[ii].getConstructor();
- if( !collectReconstructNodes( id, tchildren, dt[ii], d_reconstruct_op[id][cons], status ) ){
- d_reconstruct_op[id].erase( cons );
- status = 1;
- }else{
- Trace("csi-rcons-debug") << " identity function success for " << id << std::endl;
- break;
- }
- }
- if( status!=0 ){
- //try other options, such as matching against other constructors
- Trace("csi-rcons-debug") << "Try matching for " << id << "." << std::endl;
- bool success;
- int c_index = 0;
- do{
- success = false;
- int index_found;
- std::vector< Node > 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<args.size(); i++ ){
- Trace("csi-rcons-debug") << " " << args[i] << std::endl;
- }
- if( !collectReconstructNodes( id, args, dt[index_found], d_reconstruct_op[id][cons], status ) ){
- d_reconstruct_op[id].erase( cons );
- status = 1;
- }else{
- c_index = index_found+1;
- }
- }
- }while( success && status!=0 );
-
- if( status!=0 ){
- // construct an equivalence class of terms that are equivalent to t
- if( d_rep[id]==id ){
- Trace("csi-rcons-debug") << "Try rewriting for " << id << "." << std::endl;
- //get equivalence class of term
- std::vector< Node > 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<dt.getNumConstructors(); i++ ){
- Kind k = sti.getConsNumKind(i);
- getEquivalentTerms( k, min_t, equiv );
- }
- //assign ids to terms
- Trace("csi-rcons-debug") << "Term " << id << " is equivalent to " << equiv.size() << " terms : " << std::endl;
- std::vector< int > equiv_ids;
- for( unsigned i=0; i<equiv.size(); i++ ){
- Trace("csi-rcons-debug") << " " << equiv[i] << std::endl;
- if( d_rcons_to_id[stn].find( equiv[i] )==d_rcons_to_id[stn].end() ){
- int eq_id = allocate( equiv[i], stn );
- d_eqc.erase( eq_id );
- d_rep[eq_id] = id;
- d_eqc[id].push_back( eq_id );
- equiv_ids.push_back( eq_id );
- }else{
- equiv_ids.push_back( -1 );
- }
- }
- // now, try each of them
- for( unsigned i=0; i<equiv.size(); i++ ){
- if( equiv_ids[i]!=-1 ){
- collectReconstructNodes( equiv[i], stn, status );
- //if one succeeds
- if( status==0 ){
- Node rsol = getReconstructedSolution( equiv_ids[i] );
- Assert(!rsol.isNull());
- //set all members of the equivalence class that this is the reconstructed solution
- setReconstructed( id, rsol );
- break;
- }
- }
- }
- }else{
- Trace("csi-rcons-debug") << "Do not try rewriting for " << id << ", rep = " << d_rep[id] << std::endl;
- }
- }
- }
- }
- }
- }
- if( status!=0 ){
- Trace("csi-rcons-debug") << "-> *** 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<Node>& ts,
- const DTypeConstructor& dtc,
- std::vector<int>& ids,
- int& status)
-{
- Assert(dtc.getNumArgs() == ts.size());
- for( unsigned i=0; i<ts.size(); i++ ){
- TypeNode cstn = d_qe->getTermDatabaseSygus()->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<ids.size(); i++ ){
- d_parents[ids[i]].push_back( pid );
- }
- return true;
-}
-
-Node CegSingleInvSol::CegSingleInvSol::getReconstructedSolution(int id,
- bool mod_eq)
-{
- std::map< int, Node >::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; i<itt->second.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<d_eqc[rid].size(); i++ ){
- int tid = d_eqc[rid][i];
- if( tid!=id ){
- Node eret = getReconstructedSolution( tid, false );
- if( !eret.isNull() ){
- setReconstructed( id, eret );
- return eret;
- }
- }
- }
- }
- d_tmp_fail.push_back( id );
- return Node::null();
- }
- }
-}
-
-int CegSingleInvSol::allocate(Node n, TypeNode stn)
-{
- std::map< Node, int >::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<d_parents[rid].size(); j++ ){
- if( getPathToRoot( d_parents[rid][j] ) ){
- return true;
- }
- }
- return false;
- }
- }
-}
-
-void CegSingleInvSol::setReconstructed(int id, Node n)
-{
- //set all equivalent to this as reconstructed
- int rid = d_rep[id];
- for( unsigned i=0; i<d_eqc[rid].size(); i++ ){
- d_reconstruct[d_eqc[rid][i]] = n;
- }
-}
-
-void CegSingleInvSol::getEquivalentTerms(Kind k,
- Node n,
- std::vector<Node>& 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<bool>())
- {
- success = false;
- break;
- }
- }
- }
- if( success ){
- Node var = n[1];
- Node rem;
- if( k==PLUS || k==MINUS ){
- int rem_coeff = (int)n[0].getConst<Rational>().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<Rational>().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<d_eqt_eqc[rn].size(); i++ ){
- if( d_eqt_eqc[rn][i]!=n && d_eqt_eqc[rn][i].getKind()==k ){
- if( std::find( equiv.begin(), equiv.end(), d_eqt_eqc[rn][i] )==equiv.end() ){
- equiv.push_back( d_eqt_eqc[rn][i] );
- }
- }
- }
- }
-}
-
-void CegSingleInvSol::registerEquivalentTerms(Node n)
-{
- for( unsigned i=0; i<n.getNumChildren(); i++ ){
- registerEquivalentTerms( n[i] );
- }
- Node rn = Rewriter::rewrite( n );
- if( rn!=n ){
- Trace("csi-equiv") << " eq terms : " << n << " " << rn << std::endl;
- d_eqt_rep[n] = rn;
- d_eqt_rep[rn] = rn;
- if( std::find( d_eqt_eqc[rn].begin(), d_eqt_eqc[rn].end(), rn )==d_eqt_eqc[rn].end() ){
- d_eqt_eqc[rn].push_back( rn );
- }
- if( std::find( d_eqt_eqc[rn].begin(), d_eqt_eqc[rn].end(), n )==d_eqt_eqc[rn].end() ){
- d_eqt_eqc[rn].push_back( n );
- }
- }
-}
-
-Node CegSingleInvSol::builtinToSygusConst(Node c, TypeNode tn, int rcons_depth)
-{
- std::map<Node, Node>::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<int, Node>& s,
- std::vector<int>& 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<int> 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<Node>& args,
- int index_exc,
- int index_start)
-{
- Assert(st.isDatatype());
- const DType& dt = st.getDType();
- Assert(dt.isSygus());
- std::map<Kind, std::vector<Node> > kgens;
- std::vector<Node> 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<int, Node> sigma;
- std::vector<int> 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<int, Node>::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<Node> 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<Rational>().isNegativeOne())
- {
- mon[ro].push_back(nc);
- changed = true;
- }
- else
- {
- if (!n[r][i].isConst() || !n[r][i].getConst<Rational>().isZero())
- {
- mon[r].push_back(n[r][i]);
- }
- }
- }
- }
- else
- {
- if (ArithMSum::getMonomial(n[r], c, nc)
- && c.getConst<Rational>().isNegativeOne())
- {
- mon[ro].push_back(nc);
- changed = true;
- }
- else
- {
- if (!n[r].isConst() || !n[r].getConst<Rational>().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;
-}
-}
-}
-}
+++ /dev/null
-/********************* */
-/*! \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 <map>
-#include <vector>
-
-#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<Node>& ts,
- const DTypeConstructor& dtc,
- std::vector<int>& 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<TypeNode, std::map<Node, Node> > d_builtin_const_to_sygus;
- /** sorted list of constants, per type */
- std::map<TypeNode, std::vector<Node> > d_const_list;
- /** number of positive constants, per type */
- std::map<TypeNode, unsigned> d_const_list_pos;
- /** list of constructor indices whose operators are identity functions */
- std::map<TypeNode, std::vector<int> > 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<TypeNode, std::map<int, Node> > 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<int, Node>& s,
- std::vector<int>& 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<Node>& 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
--- /dev/null
+/********************* */
+/*! \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<Node, NodeHashFunction>&
+RConsObligationInfo::getCandidateSolutions() const
+{
+ return d_candSols;
+}
+
+void RConsObligationInfo::addCandidateSolutionToWatchSet(Node candSol)
+{
+ d_watchSet.emplace(candSol);
+}
+
+const std::unordered_set<Node, NodeHashFunction>&
+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<Node, RConsObligationInfo, NodeHashFunction>&
+ obInfo)
+{
+ std::unordered_set<Node, NodeHashFunction> visited;
+ std::vector<Node> 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<TNode, TNodeHashFunction> 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
--- /dev/null
+/********************* */
+/*! \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<Node, NodeHashFunction>& 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<Node, NodeHashFunction>& 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<Node, RConsObligationInfo, NodeHashFunction>&
+ 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<Node, NodeHashFunction> 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<Node, NodeHashFunction> d_watchSet;
+};
+
+} // namespace quantifiers
+} // namespace theory
+} // namespace CVC4
+
+#endif // CVC4__THEORY__QUANTIFIERS__RCONS_OBLIGATION_INFO_H
--- /dev/null
+/********************* */
+/*! \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<Node>& 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
--- /dev/null
+/********************* */
+/*! \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<Node>& 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<SygusEnumerator> d_enumerator;
+ /** Candidate rewrite database for this class' sygus datatype type */
+ std::unique_ptr<CandidateRewriteDatabase> 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<Node, Node, NodeHashFunction> d_ob;
+};
+
+} // namespace quantifiers
+} // namespace theory
+} // namespace CVC4
+
+#endif // CVC4__THEORY__QUANTIFIERS__RCONS_TYPE_INFO_H
--- /dev/null
+/********************* */
+/*! \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<TypeNode, std::vector<Node>, 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<const TypeNode, ObligationSet>& 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<const TypeNode, ObligationSet>& 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<const TypeNode, ObligationSet>& 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<const TypeNode, ObligationSet>& 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<Node, Node, NodeHashFunction> 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<std::pair<Node, Node>> subs;
+ Trace("sygus-rcons") << "-- ct: " << sz << std::endl;
+ // remove redundant substitutions
+ for (const std::pair<const Node, Node>& pair : d_sygusVars)
+ {
+ candObs.erase(pair.first);
+ }
+ // for each candidate obligation
+ for (const std::pair<const Node, Node>& 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<Node, Node>& 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<Node> 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<Node> 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<TypeNode> 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<const TypeNode, ObligationSet>& 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<TNode, TNodeHashFunction> vars;
+ expr::getVariables(n, vars);
+
+ std::unordered_map<TNode, TNode, TNodeHashFunction> 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<Node>& vars,
+ std::vector<Node>& 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<TypeNode, std::vector<Node>, TypeNodeHashFunction>&
+ pool) const
+{
+ Trace("sygus-rcons") << "\nPool:\n[";
+
+ for (const std::pair<const TypeNode, std::vector<Node>>& 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
--- /dev/null
+/********************* */
+/*! \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 <map>
+#include <vector>
+
+#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<Node, NodeHashFunction>;
+using TypeObligationSetMap =
+ std::unordered_map<TypeNode, ObligationSet, TypeNodeHashFunction>;
+
+/** 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<Node>& vars,
+ std::vector<Node>& 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<TypeNode,
+ std::vector<Node>,
+ 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<Node, RConsObligationInfo, NodeHashFunction> d_obInfo;
+ /** a map from a sygus datatype type to its reconstruction info */
+ std::unordered_map<TypeNode, RConsTypeInfo, TypeNodeHashFunction> d_stnInfo;
+
+ /** a map from an obligation to its sygus solution (if it exists) */
+ std::unordered_map<TNode, TNode, TNodeHashFunction> d_sol;
+
+ /** a map from a candidate solution to its sub-obligations */
+ std::unordered_map<Node, std::vector<Node>, NodeHashFunction> d_subObs;
+ /** a map from a candidate solution to its parent obligation */
+ std::unordered_map<Node, Node, NodeHashFunction> d_parentOb;
+
+ /** a cache of sygus variables treated as ground terms by matching */
+ std::unordered_map<Node, Node, NodeHashFunction> 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
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)),
Trace("cegqi-sol-debug") << "Printing synth solution..." << std::endl;
Assert(d_quant[0].getNumChildren() == d_embed_quant[0].getNumChildren());
std::vector<Node> sols;
- std::vector<int> statuses;
+ std::vector<int8_t> statuses;
if (!getSynthSolutionsInternal(sols, statuses))
{
return;
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;
{
NodeManager* nm = NodeManager::currentNM();
std::vector<Node> sols;
- std::vector<int> statuses;
+ std::vector<int8_t> statuses;
Trace("cegqi-debug") << "getSynthSolutions..." << std::endl;
if (!getSynthSolutionsInternal(sols, statuses))
{
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
}
bool SynthConjecture::getSynthSolutionsInternal(std::vector<Node>& sols,
- std::vector<int>& statuses)
+ std::vector<int8_t>& statuses)
{
if (!d_hasSolution)
{
Assert(tn.isDatatype());
// get the solution
Node sol;
- int status = -1;
+ int8_t status = -1;
if (isSingleInvocation())
{
Assert(d_ceg_si != NULL);
*/
bool checkSideCondition(const std::vector<Node>& cvals) const;
+ /** get a reference to the statistics of parent */
+ SygusStatistics& getSygusStatistics() { return d_stats; };
+
private:
/** reference to quantifier engine */
QuantifiersEngine* d_qe;
* the sygus datatype constructor corresponding to variable x.
*/
bool getSynthSolutionsInternal(std::vector<Node>& sols,
- std::vector<int>& status);
+ std::vector<int8_t>& status);
//-------------------------------- sygus stream
/**
* Prints the current synthesis solution to the output stream indicated by
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
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
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
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
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
; 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)
--- /dev/null
+; 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)
--- /dev/null
+; 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)
--- /dev/null
+; 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)
--- /dev/null
+; 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)
--- /dev/null
+; 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)
--- /dev/null
+; 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)
--- /dev/null
+; 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)
projects / cvc5.git / commitdiff