}
// if doing sygus, turn on CEGQI by default
- if(opts[options::inputLanguage] == language::input::LANG_SYGUS &&
- !opts.wasSetByUser(options::ceGuidedInst)) {
- opts.set(options::ceGuidedInst, true);
+ if(opts[options::inputLanguage] == language::input::LANG_SYGUS ){
+ if( !opts.wasSetByUser(options::ceGuidedInst)) {
+ opts.set(options::ceGuidedInst, true);
+ }
+ if( !opts.wasSetByUser(options::dumpSynth)) {
+ opts.set(options::dumpSynth, true);
+ }
}
// Determine which messages to show based on smtcomp_mode and verbosity
// make sure out and err streams are flushed too
*opts[options::out] << flush;
*opts[options::err] << flush;
-
+
#ifdef CVC4_DEBUG
if(opts[options::earlyExit] && opts.wasSetByUser(options::earlyExit)) {
_exit(returnValue);
startIndex = -1;
Debug("parser-sygus") << "Construct default grammar for " << fun << " " << range << std::endl;
std::map< CVC4::Type, CVC4::Type > sygus_to_builtin;
-
+
std::vector< Type > types;
for( unsigned i=0; i<sygus_vars.size(); i++ ){
Type t = sygus_vars[i].getType();
types.push_back( t );
}
}
-
+
//name of boolean sort
std::stringstream ssb;
ssb << fun << "_Bool";
std::string dbname = ssb.str();
Type unres_bt = mkUnresolvedType(ssb.str());
-
+
std::vector< Type > unres_types;
for( unsigned i=0; i<types.size(); i++ ){
std::stringstream ss;
// This method adds N operators to ops[index], N names to cnames[index] and N type argument vectors to cargs[index] (where typically N=1)
// This method may also add new elements pairwise into datatypes/sorts/ops/cnames/cargs in the case of non-flat gterms.
-void Smt2::processSygusGTerm( CVC4::SygusGTerm& sgt, int index,
+void Smt2::processSygusGTerm( CVC4::SygusGTerm& sgt, int index,
std::vector< CVC4::Datatype >& datatypes,
std::vector< CVC4::Type>& sorts,
std::vector< std::vector<CVC4::Expr> >& ops,
std::vector< std::vector< std::vector< CVC4::Type > > >& cargs,
std::vector< bool >& allow_const,
std::vector< std::vector< std::string > >& unresolved_gterm_sym,
- std::vector<CVC4::Expr>& sygus_vars,
- std::map< CVC4::Type, CVC4::Type >& sygus_to_builtin, std::map< CVC4::Type, CVC4::Expr >& sygus_to_builtin_expr,
+ std::vector<CVC4::Expr>& sygus_vars,
+ std::map< CVC4::Type, CVC4::Type >& sygus_to_builtin, std::map< CVC4::Type, CVC4::Expr >& sygus_to_builtin_expr,
CVC4::Type& ret, bool isNested ){
if( sgt.d_gterm_type==SygusGTerm::gterm_op || sgt.d_gterm_type==SygusGTerm::gterm_let ){
Debug("parser-sygus") << "Add " << sgt.d_expr << " to datatype " << index << std::endl;
- //convert to UMINUS if one child of -
+ Kind oldKind;
+ Kind newKind = kind::UNDEFINED_KIND;
+ //convert to UMINUS if one child of MINUS
if( sgt.d_children.size()==1 && sgt.d_expr==getExprManager()->operatorOf(kind::MINUS) ){
- sgt.d_expr = getExprManager()->operatorOf(kind::UMINUS);
+ oldKind = kind::MINUS;
+ newKind = kind::UMINUS;
+ }
+ //convert to IFF if boolean EQUAL
+ if( sgt.d_expr==getExprManager()->operatorOf(kind::EQUAL) ){
+ Type ctn = sgt.d_children[0].d_type;
+ std::map< CVC4::Type, CVC4::Type >::iterator it = sygus_to_builtin.find( ctn );
+ if( it != sygus_to_builtin.end() && it->second.isBoolean() ){
+ oldKind = kind::EQUAL;
+ newKind = kind::IFF;
+ }
+ }
+ if( newKind!=kind::UNDEFINED_KIND ){
+ Expr newExpr = getExprManager()->operatorOf(newKind);
+ Debug("parser-sygus") << "Replace " << sgt.d_expr << " with " << newExpr << std::endl;
+ sgt.d_expr = newExpr;
+ std::string oldName = kind::kindToString(oldKind);
+ std::string newName = kind::kindToString(newKind);
+ size_t pos = 0;
+ if((pos = sgt.d_name.find(oldName, pos)) != std::string::npos){
+ sgt.d_name.replace(pos, oldName.length(), newName);
+ }
}
ops[index].push_back( sgt.d_expr );
cnames[index].push_back( sgt.d_name );
int sub_dt_index = datatypes.size()-1;
//process child
Type sub_ret;
- processSygusGTerm( sgt.d_children[i], sub_dt_index, datatypes, sorts, ops, cnames, cargs, allow_const, unresolved_gterm_sym,
+ processSygusGTerm( sgt.d_children[i], sub_dt_index, datatypes, sorts, ops, cnames, cargs, allow_const, unresolved_gterm_sym,
sygus_vars, sygus_to_builtin, sygus_to_builtin_expr, sub_ret, true );
//process the nested gterm (either pop the last datatype, or flatten the argument)
- Type tt = processSygusNestedGTerm( sub_dt_index, sub_dname, datatypes, sorts, ops, cnames, cargs, allow_const, unresolved_gterm_sym,
+ Type tt = processSygusNestedGTerm( sub_dt_index, sub_dname, datatypes, sorts, ops, cnames, cargs, allow_const, unresolved_gterm_sym,
sygus_to_builtin, sygus_to_builtin_expr, sub_ret );
cargs[index].back().push_back(tt);
}
//if let, must create operator
if( sgt.d_gterm_type==SygusGTerm::gterm_let ){
- processSygusLetConstructor( sgt.d_let_vars, index, datatypes, sorts, ops, cnames, cargs,
+ processSygusLetConstructor( sgt.d_let_vars, index, datatypes, sorts, ops, cnames, cargs,
sygus_vars, sygus_to_builtin, sygus_to_builtin_expr );
}
}else if( sgt.d_gterm_type==SygusGTerm::gterm_constant ){
unresolved_gterm_sym[index].push_back(sgt.d_name);
}
}else if( sgt.d_gterm_type==SygusGTerm::gterm_ignore ){
-
+
}
}
unresolved_gterm_sym.pop_back();
return true;
}
-
+
Type Smt2::processSygusNestedGTerm( int sub_dt_index, std::string& sub_dname, std::vector< CVC4::Datatype >& datatypes,
std::vector< CVC4::Type>& sorts,
std::vector< std::vector<CVC4::Expr> >& ops,
std::vector< std::vector< std::vector< CVC4::Type > > >& cargs,
std::vector< bool >& allow_const,
std::vector< std::vector< std::string > >& unresolved_gterm_sym,
- std::map< CVC4::Type, CVC4::Type >& sygus_to_builtin,
+ std::map< CVC4::Type, CVC4::Type >& sygus_to_builtin,
std::map< CVC4::Type, CVC4::Expr >& sygus_to_builtin_expr, Type sub_ret ) {
Type t = sub_ret;
Debug("parser-sygus") << "Argument is ";
}
void Smt2::processSygusLetConstructor( std::vector< CVC4::Expr >& let_vars,
- int index,
+ int index,
std::vector< CVC4::Datatype >& datatypes,
std::vector< CVC4::Type>& sorts,
std::vector< std::vector<CVC4::Expr> >& ops,
std::vector< std::vector<std::string> >& cnames,
std::vector< std::vector< std::vector< CVC4::Type > > >& cargs,
- std::vector<CVC4::Expr>& sygus_vars,
+ std::vector<CVC4::Expr>& sygus_vars,
std::map< CVC4::Type, CVC4::Type >& sygus_to_builtin,
std::map< CVC4::Type, CVC4::Expr >& sygus_to_builtin_expr ) {
std::vector< CVC4::Expr > let_define_args;
Debug("parser-sygus") << " cons 0, selector " << j << " : " << cargs[i][0][j] << " " << bt << std::endl;
}
}
- }
+ }
*/
//last argument is the return, pop
cargs[index][dindex].pop_back();
- collectSygusLetArgs( let_body, cargs[index][dindex], let_define_args );
-
+ collectSygusLetArgs( let_body, cargs[index][dindex], let_define_args );
+
Debug("parser-sygus") << "Make define-fun with " << cargs[index][dindex].size() << " arguments..." << std::endl;
std::vector<CVC4::Type> fsorts;
for( unsigned i=0; i<cargs[index][dindex].size(); i++ ){
Debug("parser-sygus") << " " << i << " : " << let_define_args[i] << " " << let_define_args[i].getType() << " " << cargs[index][dindex][i] << std::endl;
fsorts.push_back(let_define_args[i].getType());
}
-
+
Type ft = getExprManager()->mkFunctionType(fsorts, let_body.getType());
std::stringstream ss;
ss << datatypes[index].getName() << "_let";
Expr let_func = mkFunction(ss.str(), ft, ExprManager::VAR_FLAG_DEFINED);
preemptCommand( new DefineFunctionCommand(ss.str(), let_func, let_define_args, let_body) );
-
+
ops[index].pop_back();
ops[index].push_back( let_func );
cnames[index].pop_back();
cnames[index].push_back(ss.str());
-
+
//mark function as let constructor
d_sygus_let_func_to_vars[let_func].insert( d_sygus_let_func_to_vars[let_func].end(), let_define_args.begin(), let_define_args.end() );
d_sygus_let_func_to_body[let_func] = let_body;
}
}else{
for( unsigned i=0; i<e.getNumChildren(); i++ ){
- collectSygusLetArgs( e[i], sygusArgs, builtinArgs );
- }
+ collectSygusLetArgs( e[i], sygusArgs, builtinArgs );
+ }
}
}
-void Smt2::setSygusStartIndex( std::string& fun, int startIndex,
+void Smt2::setSygusStartIndex( std::string& fun, int startIndex,
std::vector< CVC4::Datatype >& datatypes,
std::vector< CVC4::Type>& sorts,
std::vector< std::vector<CVC4::Expr> >& ops ) {
void Smt2::mkSygusDatatype( CVC4::Datatype& dt, std::vector<CVC4::Expr>& ops,
std::vector<std::string>& cnames, std::vector< std::vector< CVC4::Type > >& cargs,
- std::vector<std::string>& unresolved_gterm_sym,
+ std::vector<std::string>& unresolved_gterm_sym,
std::map< CVC4::Type, CVC4::Type >& sygus_to_builtin ) {
Debug("parser-sygus") << "Making sygus datatype " << dt.getName() << std::endl;
Debug("parser-sygus") << " add constructors..." << std::endl;
Debug("parser-sygus") << ": replace " << ops[i] << " " << ops[i].getKind() << " " << sk << std::endl;
let_body = getExprManager()->mkExpr( sk, children );
Debug("parser-sygus") << ": new body of function is " << let_body << std::endl;
-
+
Type ft = getExprManager()->mkFunctionType(fsorts, let_body.getType());
Debug("parser-sygus") << ": function type is " << ft << std::endl;
std::stringstream ss;
}
}
}
-
+
}
void Smt2::addSygusDatatypeConstructor( CVC4::Datatype& dt, CVC4::Expr op, std::string& cname, std::vector< CVC4::Type >& cargs,
output proofs after every UNSAT/VALID response
option dumpInstantiations --dump-instantiations bool :default false
output instantiations of quantified formulas after every UNSAT/VALID response
-option dumpSynth --dump-synth bool :default false
+option dumpSynth --dump-synth bool :read-write :default false
output solution for synthesis conjectures after every UNSAT/VALID response
option unsatCores produce-unsat-cores --produce-unsat-cores bool :predicate CVC4::smt::proofEnabledBuild CVC4::smt::beforeSearch :predicate-include "smt/options_handlers.h"
turn on unsat core generation
if( !options::dtForceAssignment.wasSetByUser() ){
options::dtForceAssignment.set( true );
}
+ //try to remove ITEs from quantified formulas
+ if( !options::iteDtTesterSplitQuant.wasSetByUser() ){
+ options::iteDtTesterSplitQuant.set( true );
+ }
+ if( !options::iteLiftQuant.wasSetByUser() ){
+ options::iteLiftQuant.set( quantifiers::ITE_LIFT_QUANT_MODE_ALL );
+ }
}
if( options::intWfInduction() ){
if( !options::purifyTriggers.wasSetByUser() ){
void CegConjecture::assign( QuantifiersEngine * qe, Node q ) {
Assert( d_quant.isNull() );
Assert( q.getKind()==FORALL );
+ d_assert_quant = q;
+ //register with single invocation if applicable
+ if( qe->getTermDatabase()->isQAttrSygus( d_assert_quant ) && options::cegqiSingleInv() ){
+ d_ceg_si->initialize( qe, q );
+ if( q!=d_ceg_si->d_quant ){
+ //Node red_lem = NodeManager::currentNM()->mkNode( OR, q.negate(), d_cegqi_si->d_quant );
+ //may have rewritten quantified formula (for invariant synthesis)
+ q = d_ceg_si->d_quant;
+ }
+ }
d_quant = q;
for( unsigned i=0; i<q[0].getNumChildren(); i++ ){
d_candidates.push_back( NodeManager::currentNM()->mkSkolem( "e", q[0][i].getType() ) );
}
+ Trace("cegqi") << "Base quantified fm is : " << q << std::endl;
//construct base instantiation
d_base_inst = Rewriter::rewrite( qe->getInstantiation( q, d_candidates ) );
Trace("cegqi") << "Base instantiation is : " << d_base_inst << std::endl;
- if( qe->getTermDatabase()->isQAttrSygus( q ) ){
+ if( qe->getTermDatabase()->isQAttrSygus( d_assert_quant ) ){
CegInstantiation::collectDisjuncts( d_base_inst, d_base_disj );
Trace("cegqi") << "Conjecture has " << d_base_disj.size() << " disjuncts." << std::endl;
//store the inner variables for each disjunct
}
}
d_syntax_guided = true;
- if( options::cegqiSingleInv() ){
- d_ceg_si->initialize( qe, q );
- }
- }else if( qe->getTermDatabase()->isQAttrSynthesis( q ) ){
+ }else if( qe->getTermDatabase()->isQAttrSynthesis( d_assert_quant ) ){
d_syntax_guided = false;
}else{
Assert( false );
//d_guard_assertions[lit] = pol;
d_conj->d_infeasible = !pol;
}
- if( lit==d_conj->d_quant ){
+ if( lit==d_conj->d_assert_quant ){
d_conj->d_active = true;
}
}
Trace("cegqi-debug") << "CEGQI : Decide next on : " << d_conj->d_guard << "..." << std::endl;
return d_conj->d_guard;
}
-
+
if( d_conj->getCegqiFairMode()!=CEGQI_FAIR_NONE ){
Node lit = d_conj->getLiteral( d_quantEngine, d_conj->d_curr_lit.get() );
if( d_quantEngine->getValuation().hasSatValue( lit, value ) ) {
void CegInstantiation::checkCegConjecture( CegConjecture * conj ) {
Node q = conj->d_quant;
+ Node aq = conj->d_assert_quant;
Trace("cegqi-engine-debug") << "Synthesis conjecture : " << q << std::endl;
Trace("cegqi-engine-debug") << " * Candidate program/output symbol : ";
for( unsigned i=0; i<conj->d_candidates.size(); i++ ){
if( conj->d_ce_sk.empty() ){
Trace("cegqi-engine") << " *** Check candidate phase..." << std::endl;
- if( getTermDatabase()->isQAttrSygus( q ) ){
+ if( conj->d_syntax_guided ){
if( conj->d_ceg_si ){
std::vector< Node > lems;
conj->d_ceg_si->check( lems );
conj->d_ce_sk.push_back( std::vector< Node >() );
}
std::vector< Node > ic;
- ic.push_back( q.negate() );
+ ic.push_back( aq.negate() );
std::vector< Node > d;
collectDisjuncts( inst, d );
Assert( d.size()==conj->d_base_disj.size() );
Trace("cegqi-engine") << " ...find counterexample." << std::endl;
}
- }else if( getTermDatabase()->isQAttrSynthesis( q ) ){
+ }else{
+ Assert( aq==q );
std::vector< Node > model_terms;
if( getModelValues( conj, conj->d_candidates, model_terms ) ){
d_quantEngine->addInstantiation( q, model_terms, false );
// out << "Solution:" << std::endl;
//}
for( unsigned i=0; i<d_conj->d_candidates.size(); i++ ){
+ Node prog = d_conj->d_quant[0][i];
std::stringstream ss;
- ss << d_conj->d_quant[0][i];
+ ss << prog;
std::string f(ss.str());
f.erase(f.begin());
- TypeNode tn = d_conj->d_quant[0][i].getType();
+ TypeNode tn = prog.getType();
Assert( datatypes::DatatypesRewriter::isTypeDatatype( tn ) );
const Datatype& dt = ((DatatypeType)(tn).toType()).getDatatype();
Assert( dt.isSygus() );
}else{
if( !d_conj->d_candidate_inst[i].empty() ){
sol = d_conj->d_candidate_inst[i].back();
- status = 1;
+ //check if this was based on a template, if so, we must do reconstruction
+ if( d_conj->d_assert_quant!=d_conj->d_quant ){
+ Trace("cegqi-inv") << "Sygus version of solution is : " << sol << ", type : " << sol.getType() << std::endl;
+ sol = getTermDatabase()->getTermDatabaseSygus()->sygusToBuiltin( sol, sol.getType() );
+ Trace("cegqi-inv") << "Builtin version of solution is : " << sol << ", type : " << sol.getType() << std::endl;
+ std::vector< Node > subs;
+ Expr svl = dt.getSygusVarList();
+ for( unsigned j=0; j<svl.getNumChildren(); j++ ){
+ subs.push_back( Node::fromExpr( svl[j] ) );
+ }
+ if( options::sygusInvTemplMode() == SYGUS_INV_TEMPL_MODE_PRE ){
+ Node pre = d_conj->d_ceg_si->d_trans_pre[prog];
+ pre = pre.substitute( d_conj->d_ceg_si->d_prog_templ_vars[prog].begin(), d_conj->d_ceg_si->d_prog_templ_vars[prog].end(),
+ subs.begin(), subs.end() );
+ sol = NodeManager::currentNM()->mkNode( OR, sol, pre );
+ }else if( options::sygusInvTemplMode() == SYGUS_INV_TEMPL_MODE_POST ){
+ Node post = d_conj->d_ceg_si->d_trans_post[prog];
+ post = post.substitute( d_conj->d_ceg_si->d_prog_templ_vars[prog].begin(), d_conj->d_ceg_si->d_prog_templ_vars[prog].end(),
+ subs.begin(), subs.end() );
+ sol = NodeManager::currentNM()->mkNode( AND, sol, post );
+ }
+ Trace("cegqi-inv-debug") << "With template : " << sol << std::endl;
+ sol = Rewriter::rewrite( sol );
+ Trace("cegqi-inv-debug") << "Simplified : " << sol << std::endl;
+ sol = d_conj->d_ceg_si->reconstructToSyntax( sol, tn, status );
+ }else{
+ status = 1;
+ }
}
}
if( !(Trace.isOn("cegqi-stats")) ){
context::CDO< bool > d_active;
/** is conjecture infeasible */
context::CDO< bool > d_infeasible;
- /** quantified formula */
+ /** quantified formula asserted */
+ Node d_assert_quant;
+ /** quantified formula (after processing) */
Node d_quant;
/** guard */
Node d_guard;
}
//collect information about conjunctions
bool singleInvocation = false;
+ bool invExtractPrePost = false;
if( analyzeSygusConjunct( Node::null(), q[1], children, prog_invoke, progs, contains, true ) ){
singleInvocation = true;
//try to phrase as single invocation property
for( std::map< Node, std::vector< Node > >::iterator it2 = itp->second.begin(); it2 != itp->second.end(); ++it2 ){
if( it2->second.size()>1 ){
singleInvocation = false;
- break;
}else if( it2->second.size()==1 ){
Node prog = it2->first;
Node inv = it2->second[0];
single_invoke_args[prog][k-1].push_back( arg );
}
}
+ if( inv.getType().isBoolean() ){
+ //conjunct defines pre and/or post conditions
+ if( options::sygusInvTemplMode() != SYGUS_INV_TEMPL_MODE_NONE ){
+ invExtractPrePost = true;
+ }
+ }
}
}
}
}
}
- if( singleInvocation ){
+ if( singleInvocation || invExtractPrePost ){
+ //no value in extracting pre/post if we are single invocation
+ if( singleInvocation ){
+ invExtractPrePost = false;
+ }
Trace("cegqi-si") << "Property is single invocation with : " << std::endl;
std::vector< Node > pbvs;
std::vector< Node > new_vars;
+ std::map< Node, std::vector< Node > > prog_vars;
std::map< Node, std::vector< Node > > new_assumptions;
for( std::map< Node, std::vector< Node > >::iterator it = invocations.begin(); it != invocations.end(); ++it ){
Assert( !it->second.empty() );
Assert( !single_invoke_args[prog][k-1].empty() );
if( single_invoke_args[prog][k-1].size()==1 && single_invoke_args[prog][k-1][0].getKind()==BOUND_VARIABLE ){
invc.push_back( single_invoke_args[prog][k-1][0] );
+ prog_vars[prog].push_back( single_invoke_args[prog][k-1][0] );
}else{
//introduce fresh variable, assign all
Node v = NodeManager::currentNM()->mkSkolem( "a", single_invoke_args[prog][k-1][0].getType(), "single invocation arg" );
new_vars.push_back( v );
invc.push_back( v );
d_single_inv_arg_sk.push_back( v );
+ prog_vars[prog].push_back( v );
for( unsigned i=0; i<single_invoke_args[prog][k-1].size(); i++ ){
Node arg = single_invoke_args[prog][k-1][i];
}
//construct the single invocation version of the property
Trace("cegqi-si") << "Single invocation formula conjuncts are : " << std::endl;
- //std::vector< Node > si_conj;
Node pbvl;
if( !pbvs.empty() ){
pbvl = NodeManager::currentNM()->mkNode( BOUND_VAR_LIST, pbvs );
//should hold since we prevent miniscoping
Assert( d_single_inv.isNull() );
std::vector< Node > conjuncts;
+ std::vector< Node > conjuncts_si_progs;
+ std::vector< Node > conjuncts_si_invokes;
for( unsigned i=0; i<it->second.size(); i++ ){
Node c = it->second[i];
std::vector< Node > disj;
if( itp!=prog_invoke.end() ){
std::vector< Node > terms;
std::vector< Node > subs;
+ std::vector< Node > progs;
for( std::map< Node, std::vector< Node > >::iterator it2 = itp->second.begin(); it2 != itp->second.end(); ++it2 ){
- if( !it2->second.empty() ){
+ if( it2->second.size()==1 ){
Node prog = it2->first;
Node inv = it2->second[0];
Assert( it2->second.size()==1 );
terms.push_back( inv );
subs.push_back( d_single_inv_map[prog] );
+ progs.push_back( prog );
Trace("cegqi-si-debug2") << "subs : " << inv << " -> var for " << prog << " : " << d_single_inv_map[prog] << std::endl;
}
}
- cr = c.substitute( terms.begin(), terms.end(), subs.begin(), subs.end() );
+ if( singleInvocation ){
+ cr = c.substitute( terms.begin(), terms.end(), subs.begin(), subs.end() );
+ }else{
+ cr = c;
+ if( invExtractPrePost ){
+ if( terms.size()==1 ){
+ conjuncts_si_progs.push_back( progs[0] );
+ conjuncts_si_invokes.push_back( terms[0] );
+ }else if( terms.size()>1 ){
+ //abort when mixing multiple invariants? TODO
+ invExtractPrePost = false;
+ }
+ }
+ }
}else{
cr = c;
}
Node curr = disj.size()==1 ? disj[0] : NodeManager::currentNM()->mkNode( OR, disj );
curr = TermDb::simpleNegate( curr );
Trace("cegqi-si") << " " << curr;
+ if( invExtractPrePost && conjuncts.size()==conjuncts_si_progs.size() ){
+ conjuncts_si_progs.push_back( Node::null() );
+ conjuncts_si_invokes.push_back( Node::null() );
+ }
conjuncts.push_back( curr );
if( !it->first.isNull() ){
Trace("cegqi-si-debug") << " under " << it->first;
Trace("cegqi-si") << std::endl;
}
Assert( !conjuncts.empty() );
- //make the skolems for the existential
- if( !it->first.isNull() ){
- std::vector< Node > vars;
- std::vector< Node > sks;
- for( unsigned j=0; j<it->first.getNumChildren(); j++ ){
- std::stringstream ss;
- ss << "a_" << it->first[j];
- Node v = NodeManager::currentNM()->mkSkolem( ss.str(), it->first[j].getType(), "single invocation skolem" );
- vars.push_back( it->first[j] );
- sks.push_back( v );
+ //CASE 1 : rewrite based on a template for invariants
+ if( invExtractPrePost ){
+ //for invariant synthesis
+ std::map< Node, bool > has_inv;
+ std::map< Node, std::vector< Node > > inv_pre_post[2];
+ for( unsigned c=0; c<conjuncts.size(); c++ ){
+ Node inv = conjuncts_si_invokes[c];
+ Node prog = conjuncts_si_progs[c];
+ Trace("cegqi-si-inv-debug") << "Conjunct #" << c << ": " << conjuncts[c] << std::endl;
+ if( !prog.isNull() ){
+ Trace("cegqi-si-inv-debug") << "...has program " << prog << " invoked once: " << inv << std::endl;
+ std::vector< Node > curr_disj;
+ //find the polarity of the invocation : this determines pre vs. post
+ int pol = extractInvariantPolarity( conjuncts[c], inv, curr_disj, true );
+ Trace("cegqi-si-inv-debug") << "...polarity is " << pol << std::endl;
+ if( ( pol==1 && !curr_disj.empty() ) || pol==0 ){
+ //conjunct is part of pre/post condition : will add to template of invariant
+ Node nc = curr_disj.empty() ? NodeManager::currentNM()->mkConst( true ) :
+ ( curr_disj.size()==1 ? curr_disj[0] : NodeManager::currentNM()->mkNode( AND, curr_disj ) );
+ nc = pol==0 ? nc : TermDb::simpleNegate( nc );
+ Trace("cegqi-si-inv-debug") << " -> " << nc << " is " << ( pol==0 ? "pre" : "post" ) << "condition of invariant " << prog << "." << std::endl;
+ inv_pre_post[pol][prog].push_back( nc );
+ has_inv[prog] = true;
+ }
+ }
}
- //substitute conjunctions
- for( unsigned i=0; i<conjuncts.size(); i++ ){
- conjuncts[i] = conjuncts[i].substitute( vars.begin(), vars.end(), sks.begin(), sks.end() );
+ Trace("cegqi-si-inv") << "Constructing invariant templates..." << std::endl;
+ //now, contruct the template for the invariant(s)
+ std::map< Node, Node > prog_templ;
+ for( std::map< Node, bool >::iterator iti = has_inv.begin(); iti != has_inv.end(); ++iti ){
+ Node prog = iti->first;
+ Trace("cegqi-si-inv") << "...for " << prog << "..." << std::endl;
+ Trace("cegqi-si-inv") << " args : ";
+ for( unsigned j=0; j<prog_vars[prog].size(); j++ ){
+ Node v = NodeManager::currentNM()->mkBoundVar( prog_vars[prog][j].getType() );
+ d_prog_templ_vars[prog].push_back( v );
+ Trace("cegqi-si-inv") << v << " ";
+ }
+ Trace("cegqi-si-inv") << std::endl;
+ Node pre = inv_pre_post[0][prog].empty() ? NodeManager::currentNM()->mkConst( false ) :
+ ( inv_pre_post[0][prog].size()==1 ? inv_pre_post[0][prog][0] : NodeManager::currentNM()->mkNode( OR, inv_pre_post[0][prog] ) );
+ d_trans_pre[prog] = pre.substitute( prog_vars[prog].begin(), prog_vars[prog].end(), d_prog_templ_vars[prog].begin(), d_prog_templ_vars[prog].end() );
+ Node post = inv_pre_post[1][prog].empty() ? NodeManager::currentNM()->mkConst( true ) :
+ ( inv_pre_post[1][prog].size()==1 ? inv_pre_post[1][prog][0] : NodeManager::currentNM()->mkNode( AND, inv_pre_post[1][prog] ) );
+ d_trans_post[prog] = post.substitute( prog_vars[prog].begin(), prog_vars[prog].end(), d_prog_templ_vars[prog].begin(), d_prog_templ_vars[prog].end() );
+ Trace("cegqi-si-inv") << " precondition : " << d_trans_pre[prog] << std::endl;
+ Trace("cegqi-si-inv") << " postcondition : " << d_trans_post[prog] << std::endl;
+ Node invariant = d_single_inv_app_map[prog];
+ invariant = invariant.substitute( prog_vars[prog].begin(), prog_vars[prog].end(), d_prog_templ_vars[prog].begin(), d_prog_templ_vars[prog].end() );
+ Trace("cegqi-si-inv") << " invariant : " << invariant << std::endl;
+ //construct template
+ Node templ;
+ if( options::sygusInvTemplMode() == SYGUS_INV_TEMPL_MODE_PRE ){
+ //templ = NodeManager::currentNM()->mkNode( AND, NodeManager::currentNM()->mkNode( OR, d_trans_pre[prog], invariant ), d_trans_post[prog] );
+ templ = NodeManager::currentNM()->mkNode( OR, d_trans_pre[prog], invariant );
+ }else{
+ Assert( options::sygusInvTemplMode() == SYGUS_INV_TEMPL_MODE_POST );
+ //templ = NodeManager::currentNM()->mkNode( OR, d_trans_pre[prog], NodeManager::currentNM()->mkNode( AND, d_trans_post[prog], invariant ) );
+ templ = NodeManager::currentNM()->mkNode( AND, d_trans_post[prog], invariant );
+ }
+ Trace("cegqi-si-inv") << " template : " << templ << std::endl;
+ prog_templ[prog] = templ;
}
- d_single_inv_arg_sk.insert( d_single_inv_arg_sk.end(), sks.begin(), sks.end() );
- //substitute single invocation applications
- for( std::map< Node, Node >::iterator itam = d_single_inv_app_map.begin(); itam != d_single_inv_app_map.end(); ++itam ){
- Node n = itam->second;
- d_single_inv_app_map[itam->first] = n.substitute( vars.begin(), vars.end(), sks.begin(), sks.end() );
+ Node bd = conjuncts.size()==1 ? conjuncts[0] : NodeManager::currentNM()->mkNode( OR, conjuncts );
+ Trace("cegqi-si-inv") << " body : " << bd << std::endl;
+ bd = substituteInvariantTemplates( bd, prog_templ, d_prog_templ_vars );
+ Trace("cegqi-si-inv-debug") << " templ-subs body : " << bd << std::endl;
+ //make inner existential
+ std::vector< Node > new_var_bv;
+ for( unsigned j=0; j<new_vars.size(); j++ ){
+ new_var_bv.push_back( NodeManager::currentNM()->mkBoundVar( new_vars[j].getType() ) );
}
- }
- //ensure that this is a ground property
- for( std::map< Node, Node >::iterator itam = d_single_inv_app_map.begin(); itam != d_single_inv_app_map.end(); ++itam ){
- Node n = itam->second;
- //check if all variables are arguments of this
- std::vector< Node > n_args;
- for( unsigned i=1; i<n.getNumChildren(); i++ ){
- n_args.push_back( n[i] );
+ bd = bd.substitute( new_vars.begin(), new_vars.end(), new_var_bv.begin(), new_var_bv.end() );
+ for( unsigned j=0; j<q[1][0][0].getNumChildren(); j++ ){
+ new_var_bv.push_back( q[1][0][0][j] );
}
- for( int i=0; i<(int)d_single_inv_arg_sk.size(); i++ ){
- if( std::find( n_args.begin(), n_args.end(), d_single_inv_arg_sk[i] )==n_args.end() ){
- Trace("cegqi-si") << "...property is not ground: program invocation " << n << " does not contain variable " << d_single_inv_arg_sk[i] << "." << std::endl;
- //try to do variable elimination on d_single_inv_arg_sk[i]
- if( doVariableElimination( d_single_inv_arg_sk[i], conjuncts ) ){
- Trace("cegqi-si") << "...did variable elimination on " << d_single_inv_arg_sk[i] << std::endl;
- d_single_inv_arg_sk.erase( d_single_inv_arg_sk.begin() + i, d_single_inv_arg_sk.begin() + i + 1 );
- i--;
- }else{
- singleInvocation = false;
- //exit( 57 );
+ if( !new_var_bv.empty() ){
+ Node bvl = NodeManager::currentNM()->mkNode( BOUND_VAR_LIST, new_var_bv );
+ bd = NodeManager::currentNM()->mkNode( FORALL, bvl, TermDb::simpleNegate( bd ) ).negate();
+ }
+ //make outer universal
+ bd = NodeManager::currentNM()->mkNode( FORALL, q[0], bd );
+ bd = Rewriter::rewrite( bd );
+ Trace("cegqi-si-inv") << " rtempl-subs body : " << bd << std::endl;
+ d_quant = bd;
+ //CASE 2 : rewrite based on single invocation
+ }else{
+ //make the skolems for the existential
+ if( !it->first.isNull() ){
+ std::vector< Node > vars;
+ std::vector< Node > sks;
+ for( unsigned j=0; j<it->first.getNumChildren(); j++ ){
+ std::stringstream ss;
+ ss << "a_" << it->first[j];
+ Node v = NodeManager::currentNM()->mkSkolem( ss.str(), it->first[j].getType(), "single invocation skolem" );
+ vars.push_back( it->first[j] );
+ sks.push_back( v );
+ }
+ //substitute conjunctions
+ for( unsigned i=0; i<conjuncts.size(); i++ ){
+ conjuncts[i] = conjuncts[i].substitute( vars.begin(), vars.end(), sks.begin(), sks.end() );
+ }
+ d_single_inv_arg_sk.insert( d_single_inv_arg_sk.end(), sks.begin(), sks.end() );
+ //substitute single invocation applications
+ for( std::map< Node, Node >::iterator itam = d_single_inv_app_map.begin(); itam != d_single_inv_app_map.end(); ++itam ){
+ Node n = itam->second;
+ d_single_inv_app_map[itam->first] = n.substitute( vars.begin(), vars.end(), sks.begin(), sks.end() );
+ }
+ }
+ //ensure that this is a ground property
+ for( std::map< Node, Node >::iterator itam = d_single_inv_app_map.begin(); itam != d_single_inv_app_map.end(); ++itam ){
+ Node n = itam->second;
+ //check if all variables are arguments of this
+ std::vector< Node > n_args;
+ for( unsigned i=1; i<n.getNumChildren(); i++ ){
+ n_args.push_back( n[i] );
+ }
+ for( int i=0; i<(int)d_single_inv_arg_sk.size(); i++ ){
+ if( std::find( n_args.begin(), n_args.end(), d_single_inv_arg_sk[i] )==n_args.end() ){
+ Trace("cegqi-si") << "...property is not ground: program invocation " << n << " does not contain variable " << d_single_inv_arg_sk[i] << "." << std::endl;
+ //try to do variable elimination on d_single_inv_arg_sk[i]
+ if( doVariableElimination( d_single_inv_arg_sk[i], conjuncts ) ){
+ Trace("cegqi-si") << "...did variable elimination on " << d_single_inv_arg_sk[i] << std::endl;
+ d_single_inv_arg_sk.erase( d_single_inv_arg_sk.begin() + i, d_single_inv_arg_sk.begin() + i + 1 );
+ i--;
+ }else{
+ singleInvocation = false;
+ //exit( 57 );
+ }
+ break;
}
- break;
}
}
- }
- if( singleInvocation ){
- Node bd = conjuncts.size()==1 ? conjuncts[0] : NodeManager::currentNM()->mkNode( OR, conjuncts );
- if( pbvl.isNull() ){
- d_single_inv = bd;
- }else{
- d_single_inv = NodeManager::currentNM()->mkNode( FORALL, pbvl, bd );
- }
- Trace("cegqi-si-debug") << "...formula is : " << d_single_inv << std::endl;
- /*
- if( options::eMatching() && options::eMatching.wasSetByUser() ){
- Node bd = d_qe->getTermDatabase()->getInstConstantBody( d_single_inv );
- std::vector< Node > patTerms;
- std::vector< Node > exclude;
- inst::Trigger::collectPatTerms( d_qe, d_single_inv, bd, patTerms, inst::Trigger::TS_ALL, exclude );
- if( !patTerms.empty() ){
- Trace("cegqi-si-em") << "Triggers : " << std::endl;
- for( unsigned i=0; i<patTerms.size(); i++ ){
- Trace("cegqi-si-em") << " " << patTerms[i] << std::endl;
+ if( singleInvocation ){
+ Node bd = conjuncts.size()==1 ? conjuncts[0] : NodeManager::currentNM()->mkNode( OR, conjuncts );
+ if( pbvl.isNull() ){
+ d_single_inv = bd;
+ }else{
+ d_single_inv = NodeManager::currentNM()->mkNode( FORALL, pbvl, bd );
+ }
+ Trace("cegqi-si-debug") << "...formula is : " << d_single_inv << std::endl;
+ /*
+ if( options::eMatching() && options::eMatching.wasSetByUser() ){
+ Node bd = d_qe->getTermDatabase()->getInstConstantBody( d_single_inv );
+ std::vector< Node > patTerms;
+ std::vector< Node > exclude;
+ inst::Trigger::collectPatTerms( d_qe, d_single_inv, bd, patTerms, inst::Trigger::TS_ALL, exclude );
+ if( !patTerms.empty() ){
+ Trace("cegqi-si-em") << "Triggers : " << std::endl;
+ for( unsigned i=0; i<patTerms.size(); i++ ){
+ Trace("cegqi-si-em") << " " << patTerms[i] << std::endl;
+ }
}
}
+ */
}
- */
}
}
}
return false;
}
+int CegConjectureSingleInv::extractInvariantPolarity( Node n, Node inv, std::vector< Node >& curr_disj, bool pol ) {
+ if( n.getKind()==NOT ){
+ return extractInvariantPolarity( n[0], inv, curr_disj, !pol );
+ }else if( ( n.getKind()==AND && pol ) || ( n.getKind()==OR && !pol ) ){
+ int curr_pol = -1;
+ for( unsigned i=0; i<n.getNumChildren(); i++ ){
+ int eipc = extractInvariantPolarity( n[i], inv, curr_disj, pol );
+ if( eipc!=-1 ){
+ if( curr_pol==-1 ){
+ curr_pol = eipc;
+ }else{
+ return -1;
+ }
+ }else{
+ curr_disj.push_back( pol ? n[i] : TermDb::simpleNegate( n[i] ) );
+ }
+ }
+ return curr_pol;
+ }else if( n==inv ){
+ return pol ? 1 : 0;
+ }else{
+ return -1;
+ }
+}
+
+Node CegConjectureSingleInv::substituteInvariantTemplates( Node n, std::map< Node, Node >& prog_templ, std::map< Node, std::vector< Node > >& prog_templ_vars ) {
+ if( n.getKind()==APPLY_UF && n.getNumChildren()>0 ){
+ std::map< Node, Node >::iterator it = prog_templ.find( n[0] );
+ if( it!=prog_templ.end() ){
+ std::vector< Node > children;
+ for( unsigned i=1; i<n.getNumChildren(); i++ ){
+ children.push_back( n[i] );
+ }
+ std::map< Node, std::vector< Node > >::iterator itv = prog_templ_vars.find( n[0] );
+ Assert( itv!=prog_templ_vars.end() );
+ Assert( children.size()==itv->second.size() );
+ Node newc = it->second.substitute( itv->second.begin(), itv->second.end(), children.begin(), children.end() );
+ return newc;
+ }
+ }
+ bool childChanged = false;
+ std::vector< Node > children;
+ for( unsigned i=0; i<n.getNumChildren(); i++ ){
+ Node nn = substituteInvariantTemplates( n[i], prog_templ, prog_templ_vars );
+ children.push_back( nn );
+ childChanged = childChanged || ( nn!=n[i] );
+ }
+ if( childChanged ){
+ if( n.getMetaKind() == kind::metakind::PARAMETERIZED ){
+ children.insert( children.begin(), n.getOperator() );
+ }
+ return NodeManager::currentNM()->mkNode( n.getKind(), children );
+ }else{
+ return n;
+ }
+}
+
bool CegConjectureSingleInv::analyzeSygusConjunct( Node p, Node n, std::map< Node, std::vector< Node > >& children,
- std::map< Node, std::map< Node, std::vector< Node > > >& prog_invoke,
- std::vector< Node >& progs, std::map< Node, std::map< Node, bool > >& contains, bool pol ) {
+ std::map< Node, std::map< Node, std::vector< Node > > >& prog_invoke,
+ std::vector< Node >& progs, std::map< Node, std::map< Node, bool > >& contains, bool pol ) {
if( ( pol && n.getKind()==OR ) || ( !pol && n.getKind()==AND ) ){
for( unsigned i=0; i<n.getNumChildren(); i++ ){
if( !analyzeSygusConjunct( p, n[i], children, prog_invoke, progs, contains, pol ) ){
Trace("csi-sol") << "Solution (pre-simplification): " << d_orig_solution << std::endl;
s = d_sol->simplifySolution( s, stn );
Trace("csi-sol") << "Solution (post-simplification): " << s << std::endl;
+ return reconstructToSyntax( s, stn, reconstructed );
+}
+
+Node CegConjectureSingleInv::reconstructToSyntax( Node s, TypeNode stn, int& reconstructed ) {
d_solution = s;
+ const Datatype& dt = ((DatatypeType)(stn).toType()).getDatatype();
//reconstruct the solution into sygus if necessary
reconstructed = 0;
return true;
}
+
}
\ No newline at end of file
bool processSingleInvLiteral( Node lit, bool pol, std::map< Node, std::vector< Node > >& case_vals );
bool doVariableElimination( Node v, std::vector< Node >& conjuncts );
bool getVariableEliminationTerm( bool pol, bool active, Node v, Node n, TNode& s, int& status );
+ //for recognizing templates for invariant synthesis
+ int extractInvariantPolarity( Node n, Node inv, std::vector< Node >& curr_disj, bool pol );
+ Node substituteInvariantTemplates( Node n, std::map< Node, Node >& prog_templ, std::map< Node, std::vector< Node > >& prog_templ_vars );
//presolve
void collectPresolveEqTerms( Node n, std::map< Node, std::vector< Node > >& teq );
void getPresolveEqConjuncts( std::vector< Node >& vars, std::vector< Node >& terms, std::map< Node, std::vector< Node > >& teq, Node n, std::vector< Node >& conj );
public:
//lemmas produced
std::vector< Node > d_lemmas_produced;
- std::vector< std::vector< Node > > d_inst;
+ std::vector< std::vector< Node > > d_inst;
private:
std::vector< Node > d_curr_lemmas;
//add instantiation
Node d_quant;
// single invocation version of quant
Node d_single_inv;
+ // transition relation version per program
+ std::map< Node, Node > d_trans_pre;
+ std::map< Node, Node > d_trans_post;
+ std::map< Node, std::vector< Node > > d_prog_templ_vars;
public:
//get the single invocation lemma
Node getSingleInvLemma( Node guard );
void check( std::vector< Node >& lems );
//get solution
Node getSolution( unsigned sol_index, TypeNode stn, int& reconstructed );
+ //reconstruct to syntax
+ Node reconstructToSyntax( Node s, TypeNode stn, int& reconstructed );
// has ites
bool hasITEs() { return d_has_ites; }
// is single invocation
ITE_LIFT_QUANT_MODE_ALL,
} IteLiftQuantMode;
+typedef enum {
+ /** synthesize I( x ) */
+ SYGUS_INV_TEMPL_MODE_NONE,
+ /** synthesize ( pre( x ) V I( x ) ) */
+ SYGUS_INV_TEMPL_MODE_PRE,
+ /** synthesize ( post( x ) ^ I( x ) ) */
+ SYGUS_INV_TEMPL_MODE_POST,
+} SygusInvTemplMode;
+
}/* CVC4::theory::quantifiers namespace */
}/* CVC4::theory namespace */
ite lifting mode for quantified formulas
option iteCondVarSplitQuant --ite-cond-var-split-quant bool :default true
split variables occurring as conditions of ITE in quantifiers
-option iteDtTesterSplitQuant --ite-dtt-split-quant bool :default false
+option iteDtTesterSplitQuant --ite-dtt-split-quant bool :read-write :default false
split ites with dt testers as conditions
# Whether to CNF quantifier bodies
# option cnfQuant --cnf-quant bool :default false
option sygusNormalFormGlobalContent --sygus-nf-sym-content bool :default true
generalize based on content in global search space narrowing
+option sygusInvTemplMode --sygus-inv-templ=MODE CVC4::theory::quantifiers::SygusInvTemplMode :default CVC4::theory::quantifiers::SYGUS_INV_TEMPL_MODE_NONE :include "theory/quantifiers/modes.h" :handler CVC4::theory::quantifiers::stringToSygusInvTemplMode :handler-include "theory/quantifiers/options_handlers.h"
+ template mode for sygus invariant synthesis
+
# approach applied to general quantified formulas
option cbqi --cbqi bool :read-write :default false
turns on counterexample-based quantifier instantiation
+ Lift if-then-else in quantified formulas. \n\
\n\
";
+static const std::string sygusInvTemplHelp = "\
+Template modes for sygus invariant synthesis, supported by --sygus-inv-templ:\n\
+\n\
+none \n\
++ Synthesize invariant directly.\n\
+\n\
+pre \n\
++ Synthesize invariant based on weakening of precondition .\n\
+\n\
+post \n\
++ Synthesize invariant based on strengthening of postcondition. \n\
+\n\
+";
inline InstWhenMode stringToInstWhenMode(std::string option, std::string optarg, SmtEngine* smt) throw(OptionException) {
if(optarg == "pre-full") {
}
}
+inline SygusInvTemplMode stringToSygusInvTemplMode(std::string option, std::string optarg, SmtEngine* smt) throw(OptionException) {
+ if(optarg == "none" ) {
+ return SYGUS_INV_TEMPL_MODE_NONE;
+ } else if(optarg == "pre") {
+ return SYGUS_INV_TEMPL_MODE_PRE;
+ } else if(optarg == "post") {
+ return SYGUS_INV_TEMPL_MODE_POST;
+ } else if(optarg == "help") {
+ puts(sygusInvTemplHelp.c_str());
+ exit(1);
+ } else {
+ throw OptionException(std::string("unknown option for --sygus-inv-templ: `") +
+ optarg + "'. Try --sygus-inv-templ help.");
+ }
+}
+
}/* CVC4::theory::quantifiers namespace */
}/* CVC4::theory namespace */
}/* CVC4 namespace */
}
Node TermDb::getInstConstantNode( Node n, Node f ){
+ Assert( d_inst_constants.find( f )!=d_inst_constants.end() );
return convertNodeToPattern(n,f,d_vars[f],d_inst_constants[ f ]);
}
Node TermDbSygus::sygusToBuiltin( Node n, TypeNode tn ) {
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();
unsigned i = Datatype::indexOf( n.getOperator().toExpr() );
}
Node QuantifiersEngine::getInstantiation( Node f, std::vector< Node >& terms ) {
+ d_term_db->makeInstantiationConstantsFor( f );
return getInstantiation( f, d_term_db->d_inst_constants[f], terms );
}
; EXPECT: unsat
-; COMMAND-LINE: --cegqi-si
+; COMMAND-LINE: --cegqi-si --no-dump-synth
(set-logic LIA)
(synth-fun findIdx ( (y1 Int) (y2 Int) (k1 Int)) Int ((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)
; EXPECT: unsat
-; COMMAND-LINE: --cegqi-si
+; COMMAND-LINE: --cegqi-si --no-dump-synth
(set-logic LIA)
(synth-fun findSum ( (y1 Int) (y2 Int) )Int ((Start Int ( 0 1 2 y1 y2 (+ Start Start) (ite BoolExpr Start Start))) (BoolExpr Bool ((< Start Start) (<= Start Start) (> Start Start) (>= Start Start)))))
(declare-var x1 Int)
; EXPECT: unsat
-; COMMAND-LINE: --cegqi
+; COMMAND-LINE: --cegqi --no-dump-synth
(set-logic LIA)
; EXPECT: unsat
-; COMMAND-LINE: --cegqi-si
+; COMMAND-LINE: --cegqi-si --no-dump-synth
(set-logic LIA)
; EXPECT: unsat
-; COMMAND-LINE: --cegqi
+; COMMAND-LINE: --cegqi --no-dump-synth
(set-logic LIA)
; EXPECT: unsat
-; COMMAND-LINE: --cegqi --no-cegqi-si
+; COMMAND-LINE: --cegqi --no-cegqi-si --no-dump-synth
(set-logic LIA)
(synth-fun f ((x Int)) Int
((Start Int ((+ Con Con) (+ Start Start) x))
; EXPECT: unsat
-; COMMAND-LINE: --cegqi-si
+; COMMAND-LINE: --cegqi-si --no-dump-synth
(set-logic LIA)
(define-sort D (Enum (a b)))
(define-fun f ((x D)) Int (ite (= x D::a) 3 7))
; EXPECT: unsat
-; COMMAND-LINE: --cegqi
+; COMMAND-LINE: --cegqi --no-dump-synth
(set-logic BV)
(synth-fun f ((x (BitVec 32))) (BitVec 32)
((Start (BitVec 32) ((bvand Start Start)
(bvsub Start Start)
- (bvor Start Start)
- (bvadd Start Start)
- (bvxor Start Start)
+ (bvor Start Start)
+ (bvadd Start Start)
+ (bvxor Start Start)
x
- #x00000000
- #xFFFFFFFF
+ #x00000000
+ #xFFFFFFFF
#x00000001))))
(declare-var x (BitVec 32))
; EXPECT: unsat
-; COMMAND-LINE: --cegqi
+; COMMAND-LINE: --cegqi --no-dump-synth
(set-logic BV)
(Start (BitVec 64) (#x0000000000000000 #x0000000000000001 x (bvnot Start)
(shl1 Start)
- (shr1 Start)
- (shr4 Start)
- (shr16 Start)
- (bvand Start Start)
- (bvor Start Start)
- (bvxor Start Start)
- (bvadd Start Start)
- (if0 Start Start Start)
+ (shr1 Start)
+ (shr4 Start)
+ (shr16 Start)
+ (bvand Start Start)
+ (bvor Start Start)
+ (bvxor Start Start)
+ (bvadd Start Start)
+ (if0 Start Start Start)
))
)
)
; EXPECT: unsat
-; COMMAND-LINE: --cegqi-si
+; COMMAND-LINE: --cegqi-si --no-dump-synth
(set-logic LIA)
(synth-inv inv-f ((x Int) (y Int) (b Bool)))
(declare-primed-var x Int)
; EXPECT: unsat
-; COMMAND-LINE: --cegqi-si
+; COMMAND-LINE: --cegqi-si --no-dump-synth
(set-logic LIA)
(define-fun g ((x Int)) Int (ite (= x 1) 15 19))
(synth-fun f ((x Int)) Int
; EXPECT: unsat
-; COMMAND-LINE: --cegqi-si
+; COMMAND-LINE: --cegqi-si --no-dump-synth
(set-logic LIA)
(synth-fun f ((x Int) (y Int)) Int
((Start Int (x
; EXPECT: unsat
-; COMMAND-LINE: --cegqi-si
+; COMMAND-LINE: --cegqi-si --no-dump-synth
(set-logic LIA)
(synth-fun max ((x Int) (y Int)) Int
; EXPECT: unsat
-; COMMAND-LINE: --cegqi
+; COMMAND-LINE: --cegqi --no-dump-synth
(set-logic LIA)
(synth-fun addExpr1 ((x Int) (y Int)) Int
((Start Int (x
y
- 0
- 1
+ 0
+ 1
(+ Start Start)
(- Start Start)
))
(synth-fun addExpr2 ((x Int) (y Int)) Int
((Start Int (x
y
- 0
- 1
+ 0
+ 1
(+ Start Start)
(- Start Start)
))
; EXPECT: unsat
-; COMMAND-LINE: --cegqi-si
+; COMMAND-LINE: --cegqi-si --no-dump-synth
(set-logic LIA)
(synth-fun f ((x Int)) Int
((Start Int ((+ (+ Con Con) Con) x))
; EXPECT: unsat
-; COMMAND-LINE: --cegqi
+; COMMAND-LINE: --cegqi --no-dump-synth
(set-logic LIA)
(synth-fun f ((x Int)) Int
((Start Int ((+ Con Con) (+ (+ Start Start) Con) x))
; EXPECT: unsat
-; COMMAND-LINE: --cegqi-si
+; COMMAND-LINE: --cegqi-si --no-dump-synth
(set-logic LIA)
; EXPECT: unsat
-; COMMAND-LINE: --cegqi-si
+; COMMAND-LINE: --cegqi-si --no-dump-synth
(set-logic LIA)
; EXPECT: unsat
-; COMMAND-LINE: --cegqi
+; COMMAND-LINE: --cegqi --no-dump-synth
(set-logic LIA)
; EXPECT: unsat
-; COMMAND-LINE: --cegqi-si
+; COMMAND-LINE: --cegqi-si --no-dump-synth
(set-logic LIA)
; EXPECT: unsat
-; COMMAND-LINE: --cegqi-si
+; COMMAND-LINE: --cegqi-si --no-dump-synth
(set-logic BV)
(define-fun parity ((a Bool) (b Bool) (c Bool) (d Bool)) Bool
; EXPECT: unsat
-; COMMAND-LINE: --cegqi --no-cegqi-si
+; COMMAND-LINE: --cegqi --no-cegqi-si --no-dump-synth
(set-logic LIA)
(synth-fun f ((x Int)) Int
((Start Int (Term (+ Start Start)))
; EXPECT: unsat
-; COMMAND-LINE: --cegqi-si
+; COMMAND-LINE: --cegqi-si --no-dump-synth
(set-logic LIA)
;; f1 is x plus 2 ;; f2 is 2x plus 5
(define-fun let0 ((x Int) (y Int) (z Int)) Int (+ (+ y x) z))
(synth-fun f1 ((x Int)) Int
- (
- (Start Int (
- (let0 Intx CInt CInt)
- )
- )
- (Intx Int (x))
- (CInt Int (0 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15))
-
- )
+ (
+ (Start Int (
+ (let0 Intx CInt CInt)
+ )
+ )
+ (Intx Int (x))
+ (CInt Int (0 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15))
+
+ )
)
(synth-fun f2 ((x Int)) Int
- (
- (Start Int (x
- (let0 Intx Start CInt)
- )
- )
+ (
+ (Start Int (x
+ (let0 Intx Start CInt)
+ )
+ )
(Intx Int (x))
- (CInt Int (0 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15))
+ (CInt Int (0 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15))
- )
+ )
)
; EXPECT: unsat
-; COMMAND-LINE: --cegqi-si
+; COMMAND-LINE: --cegqi-si --no-dump-synth
(set-logic LIA)
(synth-fun f1 ((x Int)) Int
- (
- (Start Int (
- (let ((y Int CInt) (z Int CInt)) (+ (+ y x) z))
- )
- )
- (CInt Int (0 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15))
+ (
+ (Start Int (
+ (let ((y Int CInt) (z Int CInt)) (+ (+ y x) z))
+ )
+ )
+ (CInt Int (0 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15))
- )
+ )
)
(synth-fun f2 ((x Int)) Int
- (
- (Start Int (x
- (let ((y Int Start) (z Int CInt)) (+ (+ y x) z))
- )
- )
- (CInt Int (0 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15))
+ (
+ (Start Int (x
+ (let ((y Int Start) (z Int CInt)) (+ (+ y x) z))
+ )
+ )
+ (CInt Int (0 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15))
- )
+ )
)
(declare-var x1 Int)
(declare-var x2 Int)
; EXPECT: unsat
-; COMMAND-LINE: --cegqi
+; COMMAND-LINE: --cegqi --no-dump-synth
(set-logic LIA)
(synth-fun f ((x Int)) Int ((Start Int ((- 1)))))
(declare-var x Int)
; EXPECT: unsat
-; COMMAND-LINE: --cegqi
+; COMMAND-LINE: --cegqi --no-dump-synth
(set-logic LIA)
(synth-fun inv ((x Int)) Bool
projects / cvc5.git / commitdiff