option sygusInvTemplMode --sygus-inv-templ=MODE CVC4::theory::quantifiers::SygusInvTemplMode :default CVC4::theory::quantifiers::SYGUS_INV_TEMPL_MODE_NONE :include "options/quantifiers_modes.h" :handler stringToSygusInvTemplMode
template mode for sygus invariant synthesis
-option sygusDirectEval --sygus-direct-eval bool :default false
+option sygusDirectEval --sygus-direct-eval bool :default true
direct unfolding of evaluation functions
# approach applied to general quantified formulas
if (Theory::isLeafOf(node, theory::THEORY_BV)) {
// if it is a leaf may ask for fullModel
- value = getModelFromSatSolver(node, fullModel);
+ value = getModelFromSatSolver(node, true);
Debug("bv-equality-status")<< "TLazyBitblaster::getTermModel from VarValue" << node <<" => " << value <<"\n";
Assert ((fullModel && !value.isNull() && value.isConst()) || !fullModel);
if (!value.isNull()) {
// only shared terms could not have been bit-blasted
Assert (hasBBTerm(var) || isSharedTerm(var));
- Node const_value = getModelFromSatSolver(var, fullModel);
+ Node const_value = getModelFromSatSolver(var, true);
if(const_value != Node()) {
Debug("bitvector-model") << "EagerBitblaster::collectModelInfo (assert (= "
// only shared terms could not have been bit-blasted
Assert (hasBBTerm(var) || isSharedTerm(var));
- Node const_value = getModelFromSatSolver(var, fullModel);
+ Node const_value = getModelFromSatSolver(var, true);
Assert (const_value.isNull() || const_value.isConst());
if(const_value != Node()) {
Debug("bitvector-model") << "TLazyBitblaster::collectModelInfo (assert (= "
Node abs_a = utils::mkNode(kind::ITE, a_lt_0, utils::mkNode(kind::BITVECTOR_NEG, a), a);
Node abs_b = utils::mkNode(kind::ITE, b_lt_0, utils::mkNode(kind::BITVECTOR_NEG, b), b);
- Node a_udiv_b = utils::mkNode(kind::BITVECTOR_UDIV, abs_a, abs_b);
+ Node a_udiv_b = utils::mkNode(options::bitvectorDivByZeroConst() ? kind::BITVECTOR_UDIV_TOTAL : kind::BITVECTOR_UDIV, abs_a, abs_b);
Node neg_result = utils::mkNode(kind::BITVECTOR_NEG, a_udiv_b);
Node condition = utils::mkNode(kind::XOR, a_lt_0, b_lt_0);
Node abs_a = utils::mkNode(kind::ITE, a_lt_0, utils::mkNode(kind::BITVECTOR_NEG, a), a);
Node abs_b = utils::mkNode(kind::ITE, b_lt_0, utils::mkNode(kind::BITVECTOR_NEG, b), b);
- Node a_urem_b = utils::mkNode(kind::BITVECTOR_UREM, abs_a, abs_b);
+ Node a_urem_b = utils::mkNode( options::bitvectorDivByZeroConst() ? kind::BITVECTOR_UREM_TOTAL : kind::BITVECTOR_UREM, abs_a, abs_b);
Node neg_result = utils::mkNode(kind::BITVECTOR_NEG, a_urem_b);
Node result = utils::mkNode(kind::ITE, a_lt_0, neg_result, a_urem_b);
}
}
//push
- if( parent==NOT || parent==BITVECTOR_NOT || parent==UMINUS || parent==BITVECTOR_NEG ){
+ if( parent==NOT || parent==BITVECTOR_NOT || parent==UMINUS || parent==BITVECTOR_NEG || k==ITE ){
//negation normal form
if( parent==k && isArgDatatype( dt[c], 0, pdt ) ){
return false;
}
Kind nk = UNDEFINED_KIND;
- Kind reqk = UNDEFINED_KIND; //required kind for all children
+ Kind reqk = UNDEFINED_KIND; //required kind for all children
+ std::map< unsigned, Kind > reqkc; //required kind for some children
if( parent==NOT ){
if( k==AND ) {
nk = OR;reqk = NOT;
}else if( k==XOR ) {
nk = IFF;
}
- }
- if( parent==BITVECTOR_NOT ){
+ }else if( parent==BITVECTOR_NOT ){
if( k==BITVECTOR_AND ) {
nk = BITVECTOR_OR;reqk = BITVECTOR_NOT;
}else if( k==BITVECTOR_OR ){
}else if( k==BITVECTOR_XOR ) {
nk = BITVECTOR_XNOR;
}
- }
- if( parent==UMINUS ){
+ }else if( parent==UMINUS ){
if( k==PLUS ){
nk = PLUS;reqk = UMINUS;
}
- }
- if( parent==BITVECTOR_NEG ){
+ }else if( parent==BITVECTOR_NEG ){
if( k==PLUS ){
nk = PLUS;reqk = BITVECTOR_NEG;
}
+ }else if( k==ITE ){
+ //ITE lifting
+ if( parent!=ITE ){
+ nk = ITE;
+ reqkc[1] = parent;
+ reqkc[2] = parent;
+ }
}
if( nk!=UNDEFINED_KIND ){
Trace("sygus-split-debug") << "Push " << parent << " over " << k << " to " << nk;
int pcr = d_tds->getKindArg( tnp, nk );
if( pcr!=-1 ){
Assert( pcr<(int)pdt.getNumConstructors() );
- if( reqk!=UNDEFINED_KIND ){
+ if( reqk!=UNDEFINED_KIND || !reqkc.empty() ){
//must have same number of arguments
if( pdt[pcr].getNumArgs()==dt[c].getNumArgs() ){
- bool success = true;
- std::map< int, TypeNode > childTypes;
for( unsigned i=0; i<pdt[pcr].getNumArgs(); i++ ){
TypeNode tna = d_tds->getArgType( pdt[pcr], i );
Assert( datatypes::DatatypesRewriter::isTypeDatatype( tna ) );
+ std::vector< Kind > rks;
if( reqk!=UNDEFINED_KIND ){
- //child must have a NOT
- int nindex = d_tds->getKindArg( tna, reqk );
+ rks.push_back( reqk );
+ }
+ std::map< unsigned, Kind >::iterator itr = reqkc.find( i );
+ if( itr!=reqkc.end() ){
+ rks.push_back( itr->second );
+ }
+ for( unsigned j=0; j<rks.size(); j++ ){
+ Kind rkc = rks[j];
+ //child must have reqk
+ int nindex = d_tds->getKindArg( tna, rkc );
if( nindex!=-1 ){
const Datatype& adt = ((DatatypeType)(tn).toType()).getDatatype();
if( d_tds->getArgType( dt[c], i )!=d_tds->getArgType( adt[nindex], 0 ) ){
Trace("sygus-split-debug") << "...arg " << i << " type mismatch." << std::endl;
- success = false;
- break;
+ return true;
}
}else{
- Trace("sygus-split-debug") << "...argument " << i << " does not have " << reqk << "." << std::endl;
- success = false;
- break;
+ Trace("sygus-split-debug") << "...argument " << i << " does not have " << rkc << "." << std::endl;
+ return true;
}
- }else{
- childTypes[i] = tna;
}
}
- if( success ){
- Trace("sygus-split-debug") << "...success" << std::endl;
- return false;
- }
+ Trace("sygus-split-debug") << "...success" << std::endl;
+ return false;
}else{
Trace("sygus-split-debug") << "...#arg mismatch." << std::endl;
}
#include "theory/quantifiers/term_database.h"
#include "theory/theory_engine.h"
#include "prop/prop_engine.h"
+#include "theory/bv/theory_bv_rewriter.h"
using namespace CVC4::kind;
using namespace std;
}
}
d_quant = q;
+ Assert( d_candidates.empty() );
+ std::vector< Node > vars;
for( unsigned i=0; i<q[0].getNumChildren(); i++ ){
+ vars.push_back( q[0][i] );
d_candidates.push_back( NodeManager::currentNM()->mkSkolem( "e", q[0][i].getType() ) );
}
Trace("cegqi") << "Base quantified formula is : " << q << std::endl;
//construct base instantiation
- d_base_inst = Rewriter::rewrite( d_qe->getInstantiation( q, d_candidates ) );
+ d_base_inst = Rewriter::rewrite( d_qe->getInstantiation( q, vars, d_candidates ) );
Trace("cegqi") << "Base instantiation is : " << d_base_inst << std::endl;
if( d_qe->getTermDatabase()->isQAttrSygus( d_assert_quant ) ){
CegInstantiation::collectDisjuncts( d_base_inst, d_base_disj );
if( datatypes::DatatypesRewriter::isTypeDatatype(tn) ){
const Datatype& dt = ((DatatypeType)(tn).toType()).getDatatype();
if( dt.isSygus() ){
- //take ownership of this quantified formula (will use direct evaluation instead of instantiation)
- d_quantEngine->setOwner( q, this );
- d_eval_axioms[q] = true;
+ //do unfolding if it induces Boolean structure,
+ //do direct evaluation if it does not induce Boolean structure,
+ // the reasoning is unfolding over these terms does not lead to helpful conflict analysis, and introduces many shared terms
+ bool directEval = true;
+ TypeNode ptn = pat.getType();
+ if( ptn.isBoolean() || ptn.isBitVector() ){
+ directEval = false;
+ }else{
+ unsigned cindex = Datatype::indexOf(pat[0].getOperator().toExpr() );
+ Node base = d_quantEngine->getTermDatabaseSygus()->getGenericBase( tn, dt, cindex );
+ Trace("cegqi-debug") << "Generic base term for " << pat[0] << " is " << base << std::endl;
+ if( base.getKind()==ITE ){
+ directEval = false;
+ }
+ }
+ if( directEval ){
+ //take ownership of this quantified formula (will use direct evaluation instead of unfolding instantiation)
+ d_quantEngine->setOwner( q, this );
+ d_eval_axioms[q] = true;
+ }
}
}
}
}
if( !eager_eval_lem.empty() ){
for( unsigned j=0; j<eager_eval_lem.size(); j++ ){
- Trace("cegqi-lemma") << "Cegqi::Lemma : evaluation : " << eager_eval_lem[j] << std::endl;
- d_quantEngine->addLemma( eager_eval_lem[j] );
+ Node lem = eager_eval_lem[j];
+ if( d_quantEngine->getTheoryEngine()->isTheoryEnabled(THEORY_BV) ){
+ //FIXME: hack to incorporate hacks from BV for division by zero
+ lem = bv::TheoryBVRewriter::eliminateBVSDiv( lem );
+ }
+ Trace("cegqi-lemma") << "Cegqi::Lemma : evaluation : " << lem << std::endl;
+ d_quantEngine->addLemma( lem );
}
return;
}
}
}
//must get a counterexample to the value of the current candidate
+ Assert( conj->d_candidates.size()==model_values.size() );
Node inst = conj->d_base_inst.substitute( conj->d_candidates.begin(), conj->d_candidates.end(), model_values.begin(), model_values.end() );
//check whether we will run CEGIS on inner skolem variables
bool sk_refine = ( !conj->isGround() || conj->d_refine_count==0 );
}
Assert( subs[j-1].getType()==var_list[j-1].getType() );
}
+ Assert( vars.size()==subs.size() );
bTerm = bTerm.substitute( vars.begin(), vars.end(), subs.begin(), subs.end() );
Trace("cegqi-eager") << "Built-in term after subs : " << bTerm << std::endl;
Trace("cegqi-eager-debug") << "Types : " << bTerm.getType() << " " << n.getType() << std::endl;
return false;
}else{
Trace("cegqi-engine") << siss.str() << std::endl;
+ Assert( d_single_inv_var.size()==subs.size() );
Node lem = d_single_inv[1].substitute( d_single_inv_var.begin(), d_single_inv_var.end(), subs.begin(), subs.end() );
if( d_qe->getTermDatabase()->containsVtsTerm( lem ) ){
Trace("cegqi-engine-debug") << "Rewrite based on vts symbols..." << std::endl;
for( unsigned i=0; i<d_sip->d_all_vars.size(); i++ ){
subs.push_back( NodeManager::currentNM()->mkSkolem( "kv", d_sip->d_all_vars[i].getType(), "created for verifying nsi" ) );
}
+ Assert( d_sip->d_all_vars.size()==subs.size() );
inst = inst.substitute( d_sip->d_all_vars.begin(), d_sip->d_all_vars.end(), subs.begin(), subs.end() );
Trace("cegqi-nsi") << "NSI : verification : " << inst << std::endl;
Trace("cegqi-lemma") << "Cegqi::Lemma : verification lemma : " << inst << std::endl;
std::sort( indices.begin(), indices.end(), ssii );
Trace("csi-sol") << "Construct solution" << std::endl;
s = constructSolution( indices, sol_index, 0 );
+ Assert( vars.size()==d_sol->d_varList.size() );
s = s.substitute( vars.begin(), vars.end(), d_sol->d_varList.begin(), d_sol->d_varList.end() );
}
d_orig_solution = s;
std::vector< Node > funcs;
//normalize the invocations
if( !terms.empty() ){
+ Assert( terms.size()==subs.size() );
cr = cr.substitute( terms.begin(), terms.end(), subs.begin(), subs.end() );
}
std::vector< Node > children;
}
Trace("si-prt") << std::endl;
cr = children.size()==1 ? children[0] : NodeManager::currentNM()->mkNode( OR, children );
+ Assert( terms.size()==subs.size() );
cr = cr.substitute( terms.begin(), terms.end(), subs.begin(), subs.end() );
Trace("si-prt-debug") << "...normalized invocations to " << cr << std::endl;
//now must check if it has other bound variables
}
}
}
+ Assert( terms.size()==subs.size() );
cr = cr.substitute( terms.begin(), terms.end(), subs.begin(), subs.end() );
}
cr = Rewriter::rewrite( cr );
TermDb::getBoundVars( cr, d_all_vars );
if( singleInvocation ){
//replace with single invocation formulation
+ Assert( si_terms.size()==si_subs.size() );
cr = cr.substitute( si_terms.begin(), si_terms.end(), si_subs.begin(), si_subs.end() );
cr = Rewriter::rewrite( cr );
Trace("si-prt") << ".....si version=" << cr << std::endl;
std::map< Node, Node >::iterator it = d_sygus_to_builtin[tn].find( n );
if( it==d_sygus_to_builtin[tn].end() ){
Trace("sygus-db-debug") << "SygusToBuiltin : compute for " << n << ", type = " << tn << std::endl;
- Assert( n.getKind()==APPLY_CONSTRUCTOR );
const Datatype& dt = ((DatatypeType)(tn).toType()).getDatatype();
+ Assert( n.getKind()==APPLY_CONSTRUCTOR );
unsigned i = Datatype::indexOf( n.getOperator().toExpr() );
Assert( n.getNumChildren()==dt[i].getNumArgs() );
std::map< TypeNode, int > var_count;
}
}
+Node TermDbSygus::getAnchor( Node n ) {
+ if( n.getKind()==APPLY_SELECTOR_TOTAL ){
+ return getAnchor( n[0] );
+ }else{
+ return n;
+ }
+}
+
void TermDbSygus::registerEvalTerm( Node n ) {
if( options::sygusDirectEval() ){
- if( n.getKind()==APPLY_UF ){
+ if( n.getKind()==APPLY_UF && !n.getType().isBoolean() ){
Trace("sygus-eager") << "TermDbSygus::eager: Register eval term : " << n << std::endl;
TypeNode tn = n[0].getType();
if( datatypes::DatatypesRewriter::isTypeDatatype(tn) ){
if( dt.isSygus() ){
Node f = n.getOperator();
Trace("sygus-eager") << "...the evaluation function is : " << f << std::endl;
- Assert( n[0].getKind()!=APPLY_CONSTRUCTOR );
- d_evals[n[0]].push_back( n );
- TypeNode tn = n[0].getType();
- Assert( datatypes::DatatypesRewriter::isTypeDatatype(tn) );
- const Datatype& dt = ((DatatypeType)(tn).toType()).getDatatype();
- Node var_list = Node::fromExpr( dt.getSygusVarList() );
- Assert( dt.isSygus() );
- d_eval_args[n[0]].push_back( std::vector< Node >() );
- for( unsigned j=1; j<n.getNumChildren(); j++ ){
- if( var_list[j-1].getType().isBoolean() ){
- //TODO: remove this case when boolean term conversion is eliminated
- Node c = NodeManager::currentNM()->mkConst(BitVector(1u, 1u));
- d_eval_args[n[0]].back().push_back( n[j].eqNode( c ) );
- }else{
- d_eval_args[n[0]].back().push_back( n[j] );
+ if( n[0].getKind()!=APPLY_CONSTRUCTOR ){
+ d_evals[n[0]].push_back( n );
+ TypeNode tn = n[0].getType();
+ Assert( datatypes::DatatypesRewriter::isTypeDatatype(tn) );
+ const Datatype& dt = ((DatatypeType)(tn).toType()).getDatatype();
+ Node var_list = Node::fromExpr( dt.getSygusVarList() );
+ Assert( dt.isSygus() );
+ d_eval_args[n[0]].push_back( std::vector< Node >() );
+ for( unsigned j=1; j<n.getNumChildren(); j++ ){
+ if( var_list[j-1].getType().isBoolean() ){
+ //TODO: remove this case when boolean term conversion is eliminated
+ Node c = NodeManager::currentNM()->mkConst(BitVector(1u, 1u));
+ d_eval_args[n[0]].back().push_back( n[j].eqNode( c ) );
+ }else{
+ d_eval_args[n[0]].back().push_back( n[j] );
+ }
}
+ Node a = getAnchor( n[0] );
+ d_subterms[a][n[0]] = true;
}
-
}
}
}
}
}
-void TermDbSygus::registerModelValue( Node n, Node v, std::vector< Node >& lems ) {
- std::map< Node, std::vector< std::vector< Node > > >::iterator it = d_eval_args.find( n );
- if( it!=d_eval_args.end() && !it->second.empty() ){
- unsigned start = d_node_mv_args_proc[n][v];
- Node antec = n.eqNode( v ).negate();
- TypeNode tn = n.getType();
- Assert( datatypes::DatatypesRewriter::isTypeDatatype(tn) );
- const Datatype& dt = ((DatatypeType)(tn).toType()).getDatatype();
- Assert( dt.isSygus() );
- Trace("sygus-eager") << "TermDbSygus::eager: Register model value : " << v << " for " << n << std::endl;
- Trace("sygus-eager") << "...it has " << it->second.size() << " evaluations, already processed " << start << "." << std::endl;
- Node bTerm = d_quantEngine->getTermDatabaseSygus()->sygusToBuiltin( v, tn );
- Trace("sygus-eager") << "Built-in term : " << bTerm << std::endl;
- std::vector< Node > vars;
- Node var_list = Node::fromExpr( dt.getSygusVarList() );
- for( unsigned j=0; j<var_list.getNumChildren(); j++ ){
- vars.push_back( var_list[j] );
- }
- //for each evaluation
- for( unsigned i=start; i<it->second.size(); i++ ){
- Assert( vars.size()==it->second[i].size() );
- Node sBTerm = bTerm.substitute( vars.begin(), vars.end(), it->second[i].begin(), it->second[i].end() );
- Node lem = NodeManager::currentNM()->mkNode( n.getType().isBoolean() ? IFF : EQUAL, d_evals[n][i], sBTerm );
- lem = NodeManager::currentNM()->mkNode( OR, antec, lem );
- Trace("sygus-eager") << "Lemma : " << lem << std::endl;
- lems.push_back( lem );
- }
- d_node_mv_args_proc[n][v] = it->second.size();
+void TermDbSygus::registerModelValue( Node a, Node v, std::vector< Node >& lems ) {
+ std::map< Node, std::map< Node, bool > >::iterator its = d_subterms.find( a );
+ if( its!=d_subterms.end() ){
+ Trace("sygus-eager") << "registerModelValue : " << a << ", has " << its->second.size() << " registered subterms." << std::endl;
+ for( std::map< Node, bool >::iterator itss = its->second.begin(); itss != its->second.end(); ++itss ){
+ Node n = itss->first;
+ Trace("sygus-eager-debug") << "...process : " << n << std::endl;
+ std::map< Node, std::vector< std::vector< Node > > >::iterator it = d_eval_args.find( n );
+ if( it!=d_eval_args.end() && !it->second.empty() ){
+ TNode at = a;
+ TNode vt = v;
+ Node vn = n.substitute( at, vt );
+ vn = Rewriter::rewrite( vn );
+ unsigned start = d_node_mv_args_proc[n][vn];
+ Node antec = n.eqNode( vn ).negate();
+ TypeNode tn = n.getType();
+ Assert( datatypes::DatatypesRewriter::isTypeDatatype(tn) );
+ const Datatype& dt = ((DatatypeType)(tn).toType()).getDatatype();
+ Assert( dt.isSygus() );
+ Trace("sygus-eager") << "TermDbSygus::eager: Register model value : " << vn << " for " << n << std::endl;
+ Trace("sygus-eager") << "...it has " << it->second.size() << " evaluations, already processed " << start << "." << std::endl;
+ Node bTerm = d_quantEngine->getTermDatabaseSygus()->sygusToBuiltin( vn, tn );
+ Trace("sygus-eager") << "Built-in term : " << bTerm << std::endl;
+ std::vector< Node > vars;
+ Node var_list = Node::fromExpr( dt.getSygusVarList() );
+ for( unsigned j=0; j<var_list.getNumChildren(); j++ ){
+ vars.push_back( var_list[j] );
+ }
+ //for each evaluation
+ for( unsigned i=start; i<it->second.size(); i++ ){
+ Assert( vars.size()==it->second[i].size() );
+ Node sBTerm = bTerm.substitute( vars.begin(), vars.end(), it->second[i].begin(), it->second[i].end() );
+ Node lem = NodeManager::currentNM()->mkNode( n.getType().isBoolean() ? IFF : EQUAL, d_evals[n][i], sBTerm );
+ lem = NodeManager::currentNM()->mkNode( OR, antec, lem );
+ Trace("sygus-eager") << "Lemma : " << lem << std::endl;
+ lems.push_back( lem );
+ }
+ d_node_mv_args_proc[n][vn] = it->second.size();
+ }
+ }
}
}
private:
std::map< TypeNode, std::map< int, Node > > d_generic_base;
std::map< TypeNode, std::vector< Node > > d_generic_templ;
- Node getGenericBase( TypeNode tn, const Datatype& dt, int c );
bool getMatch( Node p, Node n, std::map< int, Node >& s );
bool getMatch2( Node p, Node n, std::map< int, Node >& s, std::vector< int >& new_s );
public:
/** get value */
Node getTypeMaxValue( TypeNode tn );
TypeNode getSygusTypeForVar( Node v );
+ Node getGenericBase( TypeNode tn, const Datatype& dt, int c );
Node mkGeneric( const Datatype& dt, int c, std::map< TypeNode, int >& var_count, std::map< int, Node >& pre );
Node sygusToBuiltin( Node n, TypeNode tn );
Node builtinToSygusConst( Node c, TypeNode tn, int rcons_depth = 0 );
/** print sygus term */
static void printSygusTerm( std::ostream& out, Node n, std::vector< Node >& lvs );
+ /** get anchor */
+ static Node getAnchor( Node n );
//for eager instantiation
private:
+ std::map< Node, std::map< Node, bool > > d_subterms;
std::map< Node, std::vector< Node > > d_evals;
std::map< Node, std::vector< std::vector< Node > > > d_eval_args;
std::map< Node, std::map< Node, unsigned > > d_node_mv_args_proc;
for( unsigned i=0; i<d_modules.size(); i++ ){
d_modules[i]->registerQuantifier( f );
}
+ //TODO: remove this
Node ceBody = d_term_db->getInstConstantBody( f );
//also register it with the strong solver
//if( options::finiteModelFind() ){
Node body;
//process partial instantiation if necessary
if( d_term_db->d_vars[q].size()!=vars.size() ){
+ Assert( vars.size()==terms.size() );
body = q[ 1 ].substitute( vars.begin(), vars.end(), terms.begin(), terms.end() );
std::vector< Node > uninst_vars;
//doing a partial instantiation, must add quantifier for all uninstantiated variables
Trace("partial-inst") << " : " << body << std::endl;
}else{
if( options::cbqi() ){
+ Assert( vars.size()==terms.size() );
body = q[ 1 ].substitute( vars.begin(), vars.end(), terms.begin(), terms.end() );
}else{
//do optimized version
}
Node QuantifiersEngine::getInstantiation( Node q, std::vector< Node >& terms, bool doVts ) {
+ Assert( d_term_db->d_vars.find( q )!=d_term_db->d_vars.end() );
return getInstantiation( q, d_term_db->d_vars[q], terms, doVts );
}
no-mention.sy \
max2-univ.sy \
strings-small.sy \
- strings-unconstrained.sy
+ strings-unconstrained.sy \
+ hd-sdiv.sy
# sygus tests currently taking too long for make regress
EXTRA_DIST = $(TESTS) \
--- /dev/null
+; EXPECT: unsat
+; COMMAND-LINE: --cegqi --no-cegqi-si --no-dump-synth
+(set-logic BV)
+
+(define-fun hd01 ((x (BitVec 32))) (BitVec 32) (bvand x #x00000001))
+
+(synth-fun f ((x (BitVec 32))) (BitVec 32)
+ ((Start (BitVec 32) ((bvsdiv Start Start)
+ (bvand Start Start)
+ x
+ #x00000001))))
+
+(declare-var y (BitVec 32))
+(constraint (= (hd01 y) (f y)))
+(check-synth)
+
projects / cvc5.git / commitdiff