theory/quantifiers/local_theory_ext.cpp \
theory/quantifiers/fun_def_process.h \
theory/quantifiers/fun_def_process.cpp \
+ theory/quantifiers/fun_def_engine.h \
+ theory/quantifiers/fun_def_engine.cpp \
theory/quantifiers/options_handlers.h \
theory/arith/theory_arith_type_rules.h \
theory/arith/type_enumerator.h \
class Type;
class ResourceManager;
+//for sygus gterm two-pass parsing
+class CVC4_PUBLIC SygusGTerm {
+public:
+ enum{
+ gterm_op,
+ gterm_let,
+ gterm_constant,
+ gterm_variable,
+ gterm_input_variable,
+ gterm_local_variable,
+ gterm_nested_sort,
+ gterm_unresolved,
+ gterm_ignore,
+ };
+ Type d_type;
+ Expr d_expr;
+ std::vector< Expr > d_let_vars;
+ unsigned d_gterm_type;
+ std::string d_name;
+ std::vector< SygusGTerm > d_children;
+
+ unsigned getNumChildren() { return d_children.size(); }
+ void addChild(){
+ d_children.push_back( SygusGTerm() );
+ }
+};
+
namespace parser {
class Input;
std::vector<std::pair<std::string, Type> > sortedVarNames;
SExpr sexpr;
CommandSequence* seq;
+ std::vector< std::vector< CVC4::SygusGTerm > > sgts;
std::vector< CVC4::Datatype > datatypes;
std::vector< std::vector<Expr> > ops;
std::vector< std::vector< std::string > > cnames;
std::vector< bool > allow_const;
std::vector< std::vector< std::string > > unresolved_gterm_sym;
bool read_syntax = false;
- int sygus_dt_index = 0;
Type sygus_ret;
std::map< CVC4::Type, CVC4::Type > sygus_to_builtin;
std::map< CVC4::Type, CVC4::Expr > sygus_to_builtin_expr;
DEFINE_SORT_TOK { PARSER_STATE->checkThatLogicIsSet(); }
symbol[name,CHECK_UNDECLARED,SYM_SORT]
{ PARSER_STATE->checkUserSymbol(name); }
- LPAREN_TOK symbolList[names,CHECK_NONE,SYM_SORT] RPAREN_TOK
- { PARSER_STATE->pushScope(true);
- for(std::vector<std::string>::const_iterator i = names.begin(),
- iend = names.end();
- i != iend;
- ++i) {
- sorts.push_back(PARSER_STATE->mkSort(*i));
+ ( LPAREN_TOK SYGUS_ENUM_TOK LPAREN_TOK symbolList[names,CHECK_NONE,SYM_SORT] RPAREN_TOK RPAREN_TOK {
+ Debug("parser-sygus") << "Defining enum datatype " << name << " with " << names.size() << " constructors." << std::endl;
+ //make datatype
+ datatypes.push_back(Datatype(name));
+ for( unsigned i=0; i<names.size(); i++ ){
+ std::string cname = name + "__Enum__" + names[i];
+ std::string testerId("is-");
+ testerId.append(cname);
+ PARSER_STATE->checkDeclaration(cname, CHECK_UNDECLARED, SYM_VARIABLE);
+ PARSER_STATE->checkDeclaration(testerId, CHECK_UNDECLARED, SYM_VARIABLE);
+ CVC4::DatatypeConstructor c(cname, testerId);
+ datatypes[0].addConstructor(c);
+ }
+ std::vector<DatatypeType> datatypeTypes = PARSER_STATE->mkMutualDatatypeTypes(datatypes);
+ $cmd = new DatatypeDeclarationCommand(datatypeTypes);
}
- }
- sortSymbol[t,CHECK_DECLARED]
- { PARSER_STATE->popScope();
- // Do NOT call mkSort, since that creates a new sort!
- // This name is not its own distinct sort, it's an alias.
- PARSER_STATE->defineParameterizedType(name, sorts, t);
- $cmd = new DefineTypeCommand(name, sorts, t);
- }
+ | sortSymbol[t,CHECK_DECLARED] {
+ PARSER_STATE->defineParameterizedType(name, sorts, t);
+ $cmd = new DefineTypeCommand(name, sorts, t);
+ }
+ )
| /* declare-var */
DECLARE_VAR_TOK { PARSER_STATE->checkThatLogicIsSet(); }
symbol[name,CHECK_UNDECLARED,SYM_VARIABLE]
sortSymbol[t,CHECK_DECLARED]
{ PARSER_STATE->mkSygusVar(name, t);
$cmd = new EmptyCommand(); }
+ | /* declare-primed-var */
+ DECLARE_PRIMED_VAR_TOK { PARSER_STATE->checkThatLogicIsSet(); }
+ symbol[name,CHECK_UNDECLARED,SYM_VARIABLE]
+ { PARSER_STATE->checkUserSymbol(name); }
+ sortSymbol[t,CHECK_DECLARED]
+ { PARSER_STATE->mkSygusVar(name, t, true);
+ $cmd = new EmptyCommand(); }
| /* declare-fun */
DECLARE_FUN_TOK { PARSER_STATE->checkThatLogicIsSet(); }
symbol[name,CHECK_UNDECLARED,SYM_VARIABLE]
$cmd = new DefineFunctionCommand(name, func, terms, expr);
}
| /* synth-fun */
- SYNTH_FUN_TOK { PARSER_STATE->checkThatLogicIsSet(); }
+ ( SYNTH_FUN_TOK | SYNTH_INV_TOK { range = EXPR_MANAGER->booleanType(); } ) { PARSER_STATE->checkThatLogicIsSet(); }
symbol[fun,CHECK_UNDECLARED,SYM_VARIABLE]
LPAREN_TOK sortedVarList[sortedVarNames] RPAREN_TOK
{ seq = new CommandSequence();
terms.clear();
terms.push_back(bvl);
}
- sortSymbol[range,CHECK_DECLARED]
+ ( sortSymbol[range,CHECK_DECLARED] )? {
+ if( range.isNull() ){
+ PARSER_STATE->parseError("Must supply return type for synth-fun.");
+ }
+ }
( LPAREN_TOK
( LPAREN_TOK
symbol[name,CHECK_NONE,SYM_VARIABLE]
startIndex = datatypes.size();
}
std::string dname = ss.str();
+ sgts.push_back( std::vector< CVC4::SygusGTerm >() );
+ sgts.back().push_back( CVC4::SygusGTerm() );
PARSER_STATE->pushSygusDatatypeDef(t, dname, datatypes, sorts, ops, cnames, cargs, allow_const, unresolved_gterm_sym);
Type unres_t;
if(!PARSER_STATE->isUnresolvedType(dname)) {
// if not unresolved, must be undeclared
+ Debug("parser-sygus") << "Make unresolved type : " << dname << std::endl;
PARSER_STATE->checkDeclaration(dname, CHECK_UNDECLARED, SYM_SORT);
unres_t = PARSER_STATE->mkUnresolvedType(dname);
}else{
+ Debug("parser-sygus") << "Get sort : " << dname << std::endl;
unres_t = PARSER_STATE->getSort(dname);
}
sygus_to_builtin[unres_t] = t;
- sygus_dt_index = datatypes.size()-1;
Debug("parser-sygus") << "--- Read sygus grammar " << name << " under function " << fun << "..." << std::endl;
Debug("parser-sygus") << " type to resolve " << unres_t << std::endl;
Debug("parser-sygus") << " builtin type " << t << std::endl;
}
// Note the official spec for NTDef is missing the ( parens )
// but they are necessary to parse SyGuS examples
- LPAREN_TOK sygusGTerm[sygus_dt_index, datatypes, sorts, fun, ops, cnames, cargs, allow_const, unresolved_gterm_sym,
- sygus_vars, sygus_to_builtin, sygus_to_builtin_expr, sygus_ret, -1]+ RPAREN_TOK
+ LPAREN_TOK ( sygusGTerm[ sgts.back().back(), fun] { sgts.back().push_back( CVC4::SygusGTerm() ); } )+
+ RPAREN_TOK { sgts.back().pop_back(); }
RPAREN_TOK
)+
RPAREN_TOK { read_syntax = true; }
{
if( !read_syntax ){
//create the default grammar
- PARSER_STATE->mkSygusDefaultGrammar( range, terms[0], fun, datatypes, sorts, ops, sygus_vars );
+ Debug("parser-sygus") << "Make default grammar..." << std::endl;
+ PARSER_STATE->mkSygusDefaultGrammar( range, terms[0], fun, datatypes, sorts, ops, sygus_vars, startIndex );
+ //set start index
+ Debug("parser-sygus") << "Set start index " << startIndex << "..." << std::endl;
+ PARSER_STATE->setSygusStartIndex( fun, startIndex, datatypes, sorts, ops );
}else{
+ Debug("parser-sygus") << "--- Process " << sgts.size() << " sygus gterms..." << std::endl;
+ for( unsigned i=0; i<sgts.size(); i++ ){
+ for( unsigned j=0; j<sgts[i].size(); j++ ){
+ Type sub_ret;
+ PARSER_STATE->processSygusGTerm( sgts[i][j], i, datatypes, sorts, ops, cnames, cargs, allow_const, unresolved_gterm_sym,
+ sygus_vars, sygus_to_builtin, sygus_to_builtin_expr, sub_ret );
+ }
+ }
//swap index if necessary
- Debug("parser-sygus") << "Making sygus datatypes..." << std::endl;
+ Debug("parser-sygus") << "--- Making sygus datatypes..." << std::endl;
for( unsigned i=0; i<datatypes.size(); i++ ){
Debug("parser-sygus") << "..." << datatypes[i].getName() << " has builtin sort " << sorts[i] << std::endl;
}
datatypes[i].setSygus( sorts[i], terms[0], allow_const[i], false );
PARSER_STATE->mkSygusDatatype( datatypes[i], ops[i], cnames[i], cargs[i], unresolved_gterm_sym[i], sygus_to_builtin );
}
- //only care about datatypes/sorts/ops past here
- if( startIndex>0 ){
- // PARSER_STATE->swapSygusStart( startIndex, datatypes, sorts, ops, cnames, cargs, allow_const, unresolved_gterm_sym );
- CVC4::Datatype tmp_dt = datatypes[0];
- Type tmp_sort = sorts[0];
- std::vector< Expr > tmp_ops;
- tmp_ops.insert( tmp_ops.end(), ops[0].begin(), ops[0].end() );
- datatypes[0] = datatypes[startIndex];
- sorts[0] = sorts[startIndex];
- ops[0].clear();
- ops[0].insert( ops[0].end(), ops[startIndex].begin(), ops[startIndex].end() );
- datatypes[startIndex] = tmp_dt;
- sorts[startIndex] = tmp_sort;
- ops[startIndex].clear();
- ops[startIndex].insert( ops[startIndex].begin(), tmp_ops.begin(), tmp_ops.end() );
- }
+ PARSER_STATE->setSygusStartIndex( fun, startIndex, datatypes, sorts, ops );
}
+ //only care about datatypes/sorts/ops past here
PARSER_STATE->popScope();
- Debug("parser-sygus") << "Make " << datatypes.size() << " mutual datatypes..." << std::endl;
+ Debug("parser-sygus") << "--- Make " << datatypes.size() << " mutual datatypes..." << std::endl;
for( unsigned i=0; i<datatypes.size(); i++ ){
Debug("parser-sygus") << " " << i << " : " << datatypes[i].getName() << std::endl;
}
$cmd = seq;
}
| /* constraint */
- CONSTRAINT_TOK { PARSER_STATE->checkThatLogicIsSet(); }
- { Debug("parser-sygus") << "Sygus : define sygus funs..." << std::endl;
+ CONSTRAINT_TOK {
+ PARSER_STATE->checkThatLogicIsSet();
+ Debug("parser-sygus") << "Sygus : define sygus funs..." << std::endl;
PARSER_STATE->defineSygusFuns();
Debug("parser-sygus") << "Sygus : read constraint..." << std::endl;
}
PARSER_STATE->addSygusConstraint(expr);
$cmd = new EmptyCommand();
}
+ | INV_CONSTRAINT_TOK {
+ PARSER_STATE->checkThatLogicIsSet();
+ Debug("parser-sygus") << "Sygus : define sygus funs..." << std::endl;
+ PARSER_STATE->defineSygusFuns();
+ Debug("parser-sygus") << "Sygus : read inv-constraint..." << std::endl;
+ }
+ ( symbol[name,CHECK_NONE,SYM_VARIABLE] {
+ if( !terms.empty() ){
+ if( !PARSER_STATE->isDefinedFunction(name) ){
+ std::stringstream ss;
+ ss << "Function " << name << " in inv-constraint is not defined.";
+ PARSER_STATE->parseError(ss.str());
+ }
+ }
+ terms.push_back( PARSER_STATE->getVariable(name) );
+ }
+ )+ {
+ if( terms.size()!=4 ){
+ PARSER_STATE->parseError("Bad syntax for inv-constraint: expected 4 arguments.");
+ }
+ //get primed variables
+ std::vector< Expr > primed[2];
+ std::vector< Expr > all;
+ for( unsigned i=0; i<2; i++ ){
+ PARSER_STATE->getSygusPrimedVars( primed[i], i==1 );
+ all.insert( all.end(), primed[i].begin(), primed[i].end() );
+ }
+ //make relevant terms
+ for( unsigned i=0; i<4; i++ ){
+ Debug("parser-sygus") << "Make inv-constraint term #" << i << "..." << std::endl;
+ Expr op = terms[i];
+ std::vector< Expr > children;
+ children.push_back( op );
+ if( i==2 ){
+ children.insert( children.end(), all.begin(), all.end() );
+ }else{
+ children.insert( children.end(), primed[0].begin(), primed[0].end() );
+ }
+ terms[i] = EXPR_MANAGER->mkExpr(kind::APPLY,children);
+ if( i==0 ){
+ std::vector< Expr > children2;
+ children2.push_back( op );
+ children2.insert( children2.end(), primed[1].begin(), primed[1].end() );
+ terms.push_back( EXPR_MANAGER->mkExpr(kind::APPLY,children2) );
+ }
+ }
+ //make constraints
+ std::vector< Expr > conj;
+ conj.push_back( EXPR_MANAGER->mkExpr(kind::IMPLIES, terms[1], terms[0] ) );
+ conj.push_back( EXPR_MANAGER->mkExpr(kind::IMPLIES, EXPR_MANAGER->mkExpr(kind::AND, terms[0], terms[2] ), terms[4] ) );
+ conj.push_back( EXPR_MANAGER->mkExpr(kind::IMPLIES, terms[0], terms[3] ) );
+ Expr ic = EXPR_MANAGER->mkExpr( kind::AND, conj );
+ Debug("parser-sygus") << "...read invariant constraint " << ic << std::endl;
+ PARSER_STATE->addSygusConstraint(ic);
+ $cmd = new EmptyCommand();
+ }
| /* check-synth */
CHECK_SYNTH_TOK { PARSER_STATE->checkThatLogicIsSet(); }
{ Expr sygusVar = EXPR_MANAGER->mkVar("sygus", EXPR_MANAGER->booleanType());
// fun is the name of the synth-fun this grammar term is for.
// 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.
-sygusGTerm[int index,
- std::vector< CVC4::Datatype >& datatypes,
- std::vector< CVC4::Type>& sorts,
- std::string& fun,
- 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< 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,
- CVC4::Type& ret, int gtermType]
+sygusGTerm[CVC4::SygusGTerm& sgt, std::string& fun]
@declarations {
- std::string name;
+ std::string name, name2;
+ bool readEnum = false;
Kind k;
Type t;
CVC4::DatatypeConstructor* ctor = NULL;
- unsigned count = 0;
std::string sname;
- // 0 builtin operator, 1 defined operator, 2 any constant, 3 any variable, 4 ignore, 5 let, -1 none
- int sub_gtermType = -1;
- Type sub_ret;
- int sub_dt_index = -1;
- std::string sub_dname;
- Type null_type;
- Expr null_expr;
std::vector< Expr > let_vars;
- int let_start_index = -1;
- //int let_end_index = -1;
- int let_end_arg_index = -1;
- Expr let_func;
+ bool readingLet = false;
}
: LPAREN_TOK
- ( builtinOp[k]
- { Debug("parser-sygus") << "Sygus grammar " << fun << " : builtin op : " << name << std::endl;
+ //read operator
+ ( builtinOp[k]{
+ Debug("parser-sygus") << "Sygus grammar " << fun << " : builtin op : " << name << std::endl;
//since we enforce satisfaction completeness, immediately convert to total version
if( k==CVC4::kind::BITVECTOR_UDIV ){
k = CVC4::kind::BITVECTOR_UDIV_TOTAL;
}
- name = kind::kindToString(k);
- sub_gtermType = 0;
- ops[index].push_back(EXPR_MANAGER->operatorOf(k));
- cnames[index].push_back( name );
+ sgt.d_name = kind::kindToString(k);
+ sgt.d_gterm_type = SygusGTerm::gterm_op;
+ sgt.d_expr = EXPR_MANAGER->operatorOf(k);
}
| LET_TOK LPAREN_TOK {
- name = std::string("let");
- sub_gtermType = 5;
- ops[index].push_back( null_expr );
- cnames[index].push_back( name );
- cargs[index].push_back( std::vector< CVC4::Type >() );
+ sgt.d_name = std::string("let");
+ sgt.d_gterm_type = SygusGTerm::gterm_let;
PARSER_STATE->pushScope(true);
- let_start_index = datatypes.size();
+ readingLet = true;
}
( LPAREN_TOK
symbol[sname,CHECK_NONE,SYM_VARIABLE]
sortSymbol[t,CHECK_DECLARED] {
Expr v = PARSER_STATE->mkBoundVar(sname,t);
- let_vars.push_back( v );
- std::stringstream ss;
- ss << datatypes[index].getName() << "_" << ops[index].size() << "_lv_" << let_vars.size();
- sub_dname = ss.str();
- PARSER_STATE->pushSygusDatatypeDef( null_type, sub_dname, datatypes, sorts, ops, cnames, cargs, allow_const, unresolved_gterm_sym );
- sub_dt_index = datatypes.size()-1;
- sub_ret = null_type;
+ sgt.d_let_vars.push_back( v );
+ sgt.addChild();
}
- sygusGTerm[sub_dt_index,datatypes,sorts,fun,ops,cnames,cargs,allow_const,unresolved_gterm_sym,
- sygus_vars,sygus_to_builtin,sygus_to_builtin_expr,sub_ret,sub_gtermType] {
- Debug("parser-sygus") << "Process argument #" << let_vars.size() << "..." << std::endl;
- Type tt = PARSER_STATE->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);
- }
- RPAREN_TOK )+ RPAREN_TOK {
- //let_end_index = datatypes.size();
- let_end_arg_index = cargs[index].back().size();
- }
+ sygusGTerm[sgt.d_children.back(), fun]
+ RPAREN_TOK )+ RPAREN_TOK
| SYGUS_CONSTANT_TOK sortSymbol[t,CHECK_DECLARED]
- { sub_gtermType = 2; allow_const[index] = true;Debug("parser-sygus") << "Sygus grammar constant." << std::endl; }
+ { sgt.d_gterm_type = SygusGTerm::gterm_constant; sgt.d_type = t;Debug("parser-sygus") << "Sygus grammar constant." << std::endl; }
| SYGUS_VARIABLE_TOK sortSymbol[t,CHECK_DECLARED]
- { sub_gtermType = 3; Debug("parser-sygus") << "Sygus grammar variable." << std::endl; }
+ { sgt.d_gterm_type = SygusGTerm::gterm_variable; sgt.d_type = t;Debug("parser-sygus") << "Sygus grammar variable." << std::endl; }
| SYGUS_LOCAL_VARIABLE_TOK sortSymbol[t,CHECK_DECLARED]
- { sub_gtermType = 4; Debug("parser-sygus") << "Sygus grammar local variable...ignore." << std::endl; }
+ { sgt.d_gterm_type = SygusGTerm::gterm_local_variable; sgt.d_type = t;Debug("parser-sygus") << "Sygus grammar local variable...ignore." << std::endl; }
| SYGUS_INPUT_VARIABLE_TOK sortSymbol[t,CHECK_DECLARED]
- { sub_gtermType = 3; Debug("parser-sygus") << "Sygus grammar (input) variable." << std::endl; }
- | symbol[name,CHECK_NONE,SYM_VARIABLE]
- {
+ { sgt.d_gterm_type = SygusGTerm::gterm_input_variable; sgt.d_type = t;Debug("parser-sygus") << "Sygus grammar (input) variable." << std::endl; }
+ | symbol[name,CHECK_NONE,SYM_VARIABLE] {
bool isBuiltinOperator = PARSER_STATE->isOperatorEnabled(name);
if(isBuiltinOperator) {
+ Debug("parser-sygus") << "Sygus grammar " << fun << " : builtin op : " << name << std::endl;
k = PARSER_STATE->getOperatorKind(name);
if( k==CVC4::kind::BITVECTOR_UDIV ){
k = CVC4::kind::BITVECTOR_UDIV_TOTAL;
}
- name = kind::kindToString(k);
- ops[index].push_back(EXPR_MANAGER->operatorOf(k));
- cnames[index].push_back( name );
- sub_gtermType = 0;
+ sgt.d_name = kind::kindToString(k);
+ sgt.d_gterm_type = SygusGTerm::gterm_op;
+ sgt.d_expr = EXPR_MANAGER->operatorOf(k);
}else{
// what is this sygus term trying to accomplish here, if the
// symbol isn't yet declared?! probably the following line will
if( !PARSER_STATE->isDefinedFunction(name) ){
PARSER_STATE->parseError(std::string("Functions in sygus grammars must be defined."));
}
- ops[index].push_back( PARSER_STATE->getVariable(name) );
- cnames[index].push_back( name );
- sub_gtermType = 1;
+ sgt.d_name = name;
+ sgt.d_gterm_type = SygusGTerm::gterm_op;
+ sgt.d_expr = PARSER_STATE->getVariable(name) ;
}
}
)
- { Debug("parser-sygus") << "Read arguments under " << name << ", gtermType = " << sub_gtermType << std::endl;
- if( sub_gtermType!=5 ){
- cargs[index].push_back( std::vector< CVC4::Type >() );
- if( !ops[index].empty() ){
- Debug("parser-sygus") << "Operator " << ops[index].back() << std::endl;
- }
- }
- //add datatype definition for argument
- count++;
- std::stringstream ss;
- ss << datatypes[index].getName() << "_" << ops[index].size() << "_arg_" << count;
- sub_dname = ss.str();
- PARSER_STATE->pushSygusDatatypeDef( null_type, sub_dname, datatypes, sorts, ops, cnames, cargs, allow_const, unresolved_gterm_sym );
- sub_dt_index = datatypes.size()-1;
- sub_ret = null_type;
- }
- ( sygusGTerm[sub_dt_index,datatypes,sorts,fun,ops,cnames,cargs,allow_const,unresolved_gterm_sym,
- sygus_vars,sygus_to_builtin,sygus_to_builtin_expr,sub_ret,sub_gtermType]
- { Debug("parser-sygus") << "Process argument #" << count << "..." << std::endl;
- Type tt = PARSER_STATE->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);
- //add next datatype definition for argument
- count++;
- std::stringstream ss;
- ss << datatypes[index].getName() << "_" << ops[index].size() << "_arg_" << count;
- sub_dname = ss.str();
- PARSER_STATE->pushSygusDatatypeDef( null_type, sub_dname, datatypes, sorts, ops, cnames, cargs, allow_const, unresolved_gterm_sym );
- sub_dt_index = datatypes.size()-1;
- sub_ret = null_type;
- } )* RPAREN_TOK
- {
- //pop argument datatype definition
- PARSER_STATE->popSygusDatatypeDef( datatypes, sorts, ops, cnames, cargs, allow_const, unresolved_gterm_sym );
- //process constant/variable case
- if( sub_gtermType==2 || sub_gtermType==3 || sub_gtermType==4 ){
- if( !cargs[index].back().empty() ){
- PARSER_STATE->parseError(std::string("Must provide single sort for constant/variable Sygus constructor."));
- }
- cargs[index].pop_back();
- Debug("parser-sygus") << "Make constructors for Constant/Variable of type " << t << ", gterm type=" << sub_gtermType << std::endl;
- if( sub_gtermType==2 ){
- std::vector< Expr > consts;
- PARSER_STATE->mkSygusConstantsForType( t, consts );
- Debug("parser-sygus") << "...made " << consts.size() << " constants." << std::endl;
- for( unsigned i=0; i<consts.size(); i++ ){
- std::stringstream ss;
- ss << consts[i];
- Debug("parser-sygus") << "...add for constant " << ss.str() << std::endl;
- ops[index].push_back( consts[i] );
- cnames[index].push_back( ss.str() );
- cargs[index].push_back( std::vector< CVC4::Type >() );
- }
- }else if( sub_gtermType==3 ){
- Debug("parser-sygus") << "...process " << sygus_vars.size() << " variables." << std::endl;
- for( unsigned i=0; i<sygus_vars.size(); i++ ){
- if( sygus_vars[i].getType()==t ){
- std::stringstream ss;
- ss << sygus_vars[i];
- Debug("parser-sygus") << "...add for variable " << ss.str() << std::endl;
- ops[index].push_back( sygus_vars[i] );
- cnames[index].push_back( ss.str() );
- cargs[index].push_back( std::vector< CVC4::Type >() );
- }
- }
- }else if( sub_gtermType==4 ){
- //local variable, TODO?
- }
- }else if( sub_gtermType==5 ){
- if( (cargs[index].back().size()-let_end_arg_index)!=1 ){
- PARSER_STATE->parseError(std::string("Must provide single body for let Sygus constructor."));
- }
- PARSER_STATE->processSygusLetConstructor( let_vars, index, let_start_index, datatypes, sorts, ops, cnames, cargs,
- sygus_vars, sygus_to_builtin, sygus_to_builtin_expr );
- PARSER_STATE->popScope();
- //remove datatypes defining body
- //while( (int)datatypes.size()>let_end_index ){
- // Debug("parser-sygus") << "Removing let body datatype " << datatypes[datatypes.size()-1].getName() << std::endl;
- // PARSER_STATE->popSygusDatatypeDef( datatypes, sorts, ops, cnames, cargs, allow_const, unresolved_gterm_sym );
- //}
- //Debug("parser-sygus") << "Done let body datatypes" << std::endl;
- }else{
- if( cargs[index].back().empty() ){
- PARSER_STATE->parseError(std::string("Must provide argument for Sygus constructor."));
- }
- }
+ //read arguments
+ { Debug("parser-sygus") << "Read arguments under " << sgt.d_name << std::endl;
+ sgt.addChild();
+ }
+ ( sygusGTerm[sgt.d_children.back(), fun]
+ { Debug("parser-sygus") << "Finished read argument #" << sgt.d_children.size() << "..." << std::endl;
+ sgt.addChild();
+ } )*
+ RPAREN_TOK {
+ //pop last child index
+ sgt.d_children.pop_back();
+ if( readingLet ){
+ PARSER_STATE->popScope();
}
+ }
| INTEGER_LITERAL
{ Debug("parser-sygus") << "Sygus grammar " << fun << " : integer literal " << AntlrInput::tokenText($INTEGER_LITERAL) << std::endl;
- ops[index].push_back(MK_CONST(Rational(AntlrInput::tokenText($INTEGER_LITERAL))));
- cnames[index].push_back( AntlrInput::tokenText($INTEGER_LITERAL) );
- cargs[index].push_back( std::vector< CVC4::Type >() );
+ sgt.d_expr = MK_CONST(Rational(AntlrInput::tokenText($INTEGER_LITERAL)));
+ sgt.d_name = AntlrInput::tokenText($INTEGER_LITERAL);
+ sgt.d_gterm_type = SygusGTerm::gterm_op;
}
| HEX_LITERAL
{ Debug("parser-sygus") << "Sygus grammar " << fun << " : hex literal " << AntlrInput::tokenText($HEX_LITERAL) << std::endl;
assert( AntlrInput::tokenText($HEX_LITERAL).find("#x") == 0 );
std::string hexString = AntlrInput::tokenTextSubstr($HEX_LITERAL, 2);
- ops[index].push_back(MK_CONST( BitVector(hexString, 16) ));
- cnames[index].push_back( AntlrInput::tokenText($HEX_LITERAL) );
- cargs[index].push_back( std::vector< CVC4::Type >() );
+ sgt.d_expr = MK_CONST( BitVector(hexString, 16) );
+ sgt.d_name = AntlrInput::tokenText($HEX_LITERAL);
+ sgt.d_gterm_type = SygusGTerm::gterm_op;
}
| BINARY_LITERAL
{ Debug("parser-sygus") << "Sygus grammar " << fun << " : binary literal " << AntlrInput::tokenText($BINARY_LITERAL) << std::endl;
assert( AntlrInput::tokenText($BINARY_LITERAL).find("#b") == 0 );
std::string binString = AntlrInput::tokenTextSubstr($BINARY_LITERAL, 2);
- ops[index].push_back(MK_CONST( BitVector(binString, 2) ));
- cnames[index].push_back( AntlrInput::tokenText($BINARY_LITERAL) );
- cargs[index].push_back( std::vector< CVC4::Type >() );
- }
- | symbol[name,CHECK_NONE,SYM_VARIABLE]
- { if( name[0] == '-' ){ //hack for unary minus
- Debug("parser-sygus") << "Sygus grammar " << fun << " : unary minus integer literal " << name << std::endl;
- ops[index].push_back(MK_CONST(Rational(name)));
- cnames[index].push_back( name );
- cargs[index].push_back( std::vector< CVC4::Type >() );
- }else if( PARSER_STATE->isDeclared(name,SYM_VARIABLE) ){
- Debug("parser-sygus") << "Sygus grammar " << fun << " : symbol " << name << std::endl;
- Expr bv = PARSER_STATE->getVariable(name);
- ops[index].push_back(bv);
- cnames[index].push_back( name );
- cargs[index].push_back( std::vector< CVC4::Type >() );
+ sgt.d_expr = MK_CONST( BitVector(binString, 2) );
+ sgt.d_name = AntlrInput::tokenText($BINARY_LITERAL);
+ sgt.d_gterm_type = SygusGTerm::gterm_op;
+ }
+ | symbol[name,CHECK_NONE,SYM_VARIABLE] ( SYGUS_ENUM_CONS_TOK symbol[name2,CHECK_NONE,SYM_VARIABLE] { readEnum = true; } )?
+ { if( readEnum ){
+ name = name + "__Enum__" + name2;
+ Debug("parser-sygus") << "Sygus grammar " << fun << " : Enum constant " << name << std::endl;
+ Expr c = PARSER_STATE->getVariable(name);
+ sgt.d_expr = MK_EXPR(kind::APPLY_CONSTRUCTOR,c);
+ sgt.d_name = name;
+ sgt.d_gterm_type = SygusGTerm::gterm_op;
}else{
- //prepend function name to base sorts when reading an operator
- std::stringstream ss;
- ss << fun << "_" << name;
- name = ss.str();
- if( PARSER_STATE->isDeclared(name, SYM_SORT) ){
- Debug("parser-sygus") << "Sygus grammar " << fun << " : nested sort " << name << std::endl;
- ret = PARSER_STATE->getSort(name);
+ if( name[0] == '-' ){ //hack for unary minus
+ Debug("parser-sygus") << "Sygus grammar " << fun << " : unary minus integer literal " << name << std::endl;
+ sgt.d_expr = MK_CONST(Rational(name));
+ sgt.d_name = name;
+ sgt.d_gterm_type = SygusGTerm::gterm_op;
+ }else if( PARSER_STATE->isDeclared(name,SYM_VARIABLE) ){
+ Debug("parser-sygus") << "Sygus grammar " << fun << " : symbol " << name << std::endl;
+ sgt.d_expr = PARSER_STATE->getVariable(name);
+ sgt.d_name = name;
+ sgt.d_gterm_type = SygusGTerm::gterm_op;
}else{
- if( gtermType==-1 ){
- Debug("parser-sygus") << "Sygus grammar " << fun << " : unresolved symbol " << name << std::endl;
- unresolved_gterm_sym[index].push_back(name);
+ //prepend function name to base sorts when reading an operator
+ std::stringstream ss;
+ ss << fun << "_" << name;
+ name = ss.str();
+ if( PARSER_STATE->isDeclared(name, SYM_SORT) ){
+ Debug("parser-sygus") << "Sygus grammar " << fun << " : nested sort " << name << std::endl;
+ sgt.d_type = PARSER_STATE->getSort(name);
+ sgt.d_gterm_type = SygusGTerm::gterm_nested_sort;
}else{
- Debug("parser-sygus") << "Sygus grammar " << fun << " : unresolved " << name << std::endl;
- ret = PARSER_STATE->mkUnresolvedType(name);
+ Debug("parser-sygus") << "Sygus grammar " << fun << " : unresolved symbol " << name << std::endl;
+ sgt.d_gterm_type = SygusGTerm::gterm_unresolved;
+ sgt.d_name = name;
}
}
}
Debug("parser") << "term: " << AntlrInput::tokenText(LT(1)) << std::endl;
Kind kind = kind::NULL_EXPR;
Expr op;
- std::string name;
+ std::string name, name2;
std::vector<Expr> args;
std::vector< std::pair<std::string, Type> > sortedVarNames;
Expr f, f2, f3, f4;
Type type;
std::string s;
bool isBuiltinOperator = false;
+ bool readLetSort = false;
}
: /* a built-in operator application */
LPAREN_TOK builtinOp[kind] termList[args,expr] RPAREN_TOK
| /* a let binding */
LPAREN_TOK LET_TOK LPAREN_TOK
{ PARSER_STATE->pushScope(true); }
- ( LPAREN_TOK symbol[name,CHECK_NONE,SYM_VARIABLE] term[expr, f2] RPAREN_TOK
+ ( LPAREN_TOK symbol[name,CHECK_NONE,SYM_VARIABLE] (term[expr, f2] | sortSymbol[type,CHECK_DECLARED] { readLetSort = true; } term[expr, f2] ) RPAREN_TOK
// this is a parallel let, so we have to save up all the contributions
// of the let and define them only later on
- { if(names.count(name) == 1) {
+ { if( readLetSort!=PARSER_STATE->sygus() ){
+ PARSER_STATE->parseError("Bad syntax for let term.");
+ }else if(names.count(name) == 1) {
std::stringstream ss;
ss << "warning: symbol `" << name << "' bound multiple times by let; the last binding will be used, shadowing earlier ones";
PARSER_STATE->warning(ss.str());
term[expr, f2]
RPAREN_TOK
{ PARSER_STATE->popScope(); }
-
+ | symbol[name,CHECK_NONE,SYM_VARIABLE] SYGUS_ENUM_CONS_TOK symbol[name2,CHECK_NONE,SYM_VARIABLE] {
+ std::string cname = name + "__Enum__" + name2;
+ Debug("parser-sygus") << "Check for enum const " << cname << std::endl;
+ expr = PARSER_STATE->getVariable(cname);
+ //expr.getType().isConstructor() && ConstructorType(expr.getType()).getArity()==0;
+ expr = MK_EXPR(CVC4::kind::APPLY_CONSTRUCTOR, expr);
+ }
/* a variable */
| symbol[name,CHECK_DECLARED,SYM_VARIABLE]
{ if( PARSER_STATE->sygus() && name[0]=='-' &&
* use as symbols in SMT-LIB */
| SET_OPTIONS_TOK { id = "set-options"; }
| DECLARE_VAR_TOK { id = "declare-var"; }
+ | DECLARE_PRIMED_VAR_TOK { id = "declare-primed-var"; }
| SYNTH_FUN_TOK { id = "synth-fun"; }
+ | SYNTH_INV_TOK { id = "synth-inv"; }
| CONSTRAINT_TOK { id = "constraint"; }
+ | INV_CONSTRAINT_TOK { id = "inv-constraint"; }
| CHECK_SYNTH_TOK { id = "check-synth"; }
)
{ PARSER_STATE->checkDeclaration(id, check, type); }
// SyGuS commands
SYNTH_FUN_TOK : 'synth-fun';
+SYNTH_INV_TOK : 'synth-inv';
CHECK_SYNTH_TOK : 'check-synth';
DECLARE_VAR_TOK : 'declare-var';
+DECLARE_PRIMED_VAR_TOK : 'declare-primed-var';
CONSTRAINT_TOK : 'constraint';
+INV_CONSTRAINT_TOK : 'inv-constraint';
SET_OPTIONS_TOK : 'set-options';
+SYGUS_ENUM_TOK : { PARSER_STATE->sygus() }? 'Enum';
+SYGUS_ENUM_CONS_TOK : { PARSER_STATE->sygus() }? '::';
SYGUS_CONSTANT_TOK : { PARSER_STATE->sygus() }? 'Constant';
SYGUS_VARIABLE_TOK : { PARSER_STATE->sygus() }? 'Variable';
SYGUS_INPUT_VARIABLE_TOK : { PARSER_STATE->sygus() }? 'InputVariable';
addOperator(kind::BITVECTOR_SLE, "bvsle");
addOperator(kind::BITVECTOR_SGT, "bvsgt");
addOperator(kind::BITVECTOR_SGE, "bvsge");
+ addOperator(kind::BITVECTOR_REDOR, "bvredor");
+ addOperator(kind::BITVECTOR_REDAND, "bvredand");
Parser::addOperator(kind::BITVECTOR_BITOF);
Parser::addOperator(kind::BITVECTOR_EXTRACT);
ss << "Unknown SyGuS background logic `" << name << "'";
parseError(ss.str());
}
- //TODO : add additional non-standard define-funs here
-
-
}
d_logicSet = true;
}
}
-void Smt2::mkSygusDefaultGrammar( const Type& range, Expr& bvl, const std::string& fun, std::vector<CVC4::Datatype>& datatypes,
- std::vector<Type>& sorts, std::vector< std::vector<Expr> >& ops, std::vector<Expr> sygus_vars ) {
+Expr Smt2::mkSygusVar(const std::string& name, const Type& type, bool isPrimed) {
+ Expr e = mkBoundVar(name, type);
+ d_sygusVars.push_back(e);
+ d_sygusVarPrimed[e] = false;
+ if( isPrimed ){
+ std::stringstream ss;
+ ss << name << "'";
+ Expr ep = mkBoundVar(ss.str(), type);
+ d_sygusVars.push_back(ep);
+ d_sygusVarPrimed[ep] = true;
+ }
+ return e;
+}
+void Smt2::mkSygusDefaultGrammar( const Type& range, Expr& bvl, const std::string& fun, std::vector<CVC4::Datatype>& datatypes,
+ std::vector<Type>& sorts, std::vector< std::vector<Expr> >& ops, std::vector<Expr> sygus_vars, int& startIndex ) {
+ 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();
+ if( !t.isBoolean() && std::find( types.begin(), types.end(), t )==types.end() ){
+ 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;
+ ss << fun << "_" << types[i];
+ std::string dname = ss.str();
+ datatypes.push_back(Datatype(dname));
+ ops.push_back(std::vector<Expr>());
+ std::vector<std::string> cnames;
+ std::vector<std::vector<CVC4::Type> > cargs;
+ std::vector<std::string> unresolved_gterm_sym;
+ //make unresolved type
+ Type unres_t = mkUnresolvedType(dname);
+ unres_types.push_back(unres_t);
+ //add variables
+ for( unsigned j=0; j<sygus_vars.size(); j++ ){
+ if( sygus_vars[j].getType()==types[i] ){
+ std::stringstream ss;
+ ss << sygus_vars[j];
+ Debug("parser-sygus") << "...add for variable " << ss.str() << std::endl;
+ ops.back().push_back( sygus_vars[j] );
+ cnames.push_back( ss.str() );
+ cargs.push_back( std::vector< CVC4::Type >() );
+ }
+ }
+ //add constants
+ std::vector< Expr > consts;
+ mkSygusConstantsForType( types[i], consts );
+ for( unsigned j=0; j<consts.size(); j++ ){
+ std::stringstream ss;
+ ss << consts[j];
+ Debug("parser-sygus") << "...add for constant " << ss.str() << std::endl;
+ ops.back().push_back( consts[j] );
+ cnames.push_back( ss.str() );
+ cargs.push_back( std::vector< CVC4::Type >() );
+ }
+ //ITE
+ CVC4::Kind k = kind::ITE;
+ Debug("parser-sygus") << "...add for " << k << std::endl;
+ ops.back().push_back(getExprManager()->operatorOf(k));
+ cnames.push_back( kind::kindToString(k) );
+ cargs.push_back( std::vector< CVC4::Type >() );
+ cargs.back().push_back(unres_bt);
+ cargs.back().push_back(unres_t);
+ cargs.back().push_back(unres_t);
+
+ if( types[i].isInteger() ){
+ for( unsigned j=0; j<2; j++ ){
+ CVC4::Kind k = j==0 ? kind::PLUS : kind::MINUS;
+ Debug("parser-sygus") << "...add for " << k << std::endl;
+ ops.back().push_back(getExprManager()->operatorOf(k));
+ cnames.push_back(kind::kindToString(k));
+ cargs.push_back( std::vector< CVC4::Type >() );
+ cargs.back().push_back(unres_t);
+ cargs.back().push_back(unres_t);
+ }
+ }else{
+ std::stringstream sserr;
+ sserr << "No implementation for default Sygus grammar of type " << types[i] << std::endl;
+ warning(sserr.str());
+ }
+ Debug("parser-sygus") << "...make datatype " << datatypes.back() << std::endl;
+ datatypes.back().setSygus( types[i], bvl, true, true );
+ mkSygusDatatype( datatypes.back(), ops.back(), cnames, cargs, unresolved_gterm_sym, sygus_to_builtin );
+ sorts.push_back( types[i] );
+ //set start index if applicable
+ if( types[i]==range ){
+ startIndex = i;
+ }
+ }
- std::stringstream ss;
- ss << fun << "_" << range;
- std::string dname = ss.str();
- datatypes.push_back(Datatype(dname));
+ //make Boolean type
+ Type btype = getExprManager()->booleanType();
+ datatypes.push_back(Datatype(dbname));
ops.push_back(std::vector<Expr>());
std::vector<std::string> cnames;
std::vector<std::vector<CVC4::Type> > cargs;
std::vector<std::string> unresolved_gterm_sym;
- //variables
+ //add variables
for( unsigned i=0; i<sygus_vars.size(); i++ ){
- if( sygus_vars[i].getType()==range ){
+ if( sygus_vars[i].getType().isBoolean() ){
std::stringstream ss;
ss << sygus_vars[i];
Debug("parser-sygus") << "...add for variable " << ss.str() << std::endl;
cargs.push_back( std::vector< CVC4::Type >() );
}
}
- //constants
- std::vector< Expr > consts;
- mkSygusConstantsForType( range, consts );
- for( unsigned i=0; i<consts.size(); i++ ){
- std::stringstream ss;
- ss << consts[i];
- Debug("parser-sygus") << "...add for constant " << ss.str() << std::endl;
- ops.back().push_back( consts[i] );
- cnames.push_back( ss.str() );
- cargs.push_back( std::vector< CVC4::Type >() );
- }
- //ITE
- CVC4::Kind k = kind::ITE;
- Debug("parser-sygus") << "...add for " << k << std::endl;
- ops.back().push_back(getExprManager()->operatorOf(k));
- cnames.push_back( kind::kindToString(k) );
- cargs.push_back( std::vector< CVC4::Type >() );
- cargs.back().push_back(mkUnresolvedType(ssb.str()));
- cargs.back().push_back(mkUnresolvedType(ss.str()));
- cargs.back().push_back(mkUnresolvedType(ss.str()));
-
- if( range.isInteger() ){
- for( unsigned i=0; i<2; i++ ){
- CVC4::Kind k = i==0 ? kind::PLUS : kind::MINUS;
- Debug("parser-sygus") << "...add for " << k << std::endl;
- ops.back().push_back(getExprManager()->operatorOf(k));
- cnames.push_back(kind::kindToString(k));
+ //add constants if no variables and no connected types
+ if( ops.back().empty() && types.empty() ){
+ std::vector< Expr > consts;
+ mkSygusConstantsForType( btype, consts );
+ for( unsigned j=0; j<consts.size(); j++ ){
+ std::stringstream ss;
+ ss << consts[j];
+ Debug("parser-sygus") << "...add for constant " << ss.str() << std::endl;
+ ops.back().push_back( consts[j] );
+ cnames.push_back( ss.str() );
cargs.push_back( std::vector< CVC4::Type >() );
- cargs.back().push_back(mkUnresolvedType(ss.str()));
- cargs.back().push_back(mkUnresolvedType(ss.str()));
}
- }else{
- std::stringstream sserr;
- sserr << "Don't know default Sygus grammar for type " << range << std::endl;
- parseError(sserr.str());
}
- Debug("parser-sygus") << "...make datatype " << datatypes.back() << std::endl;
- datatypes.back().setSygus( range, bvl, true, true );
- mkSygusDatatype( datatypes.back(), ops.back(), cnames, cargs, unresolved_gterm_sym, sygus_to_builtin );
- sorts.push_back( range );
-
- //Boolean type
- datatypes.push_back(Datatype(dbname));
- ops.push_back(std::vector<Expr>());
- cnames.clear();
- cargs.clear();
- for( unsigned i=0; i<4; i++ ){
- CVC4::Kind k = i==0 ? kind::NOT : ( i==1 ? kind::AND : ( i==2 ? kind::OR : kind::EQUAL ) );
+ //add operators
+ for( unsigned i=0; i<3; i++ ){
+ CVC4::Kind k = i==0 ? kind::NOT : ( i==1 ? kind::AND : kind::OR );
Debug("parser-sygus") << "...add for " << k << std::endl;
ops.back().push_back(getExprManager()->operatorOf(k));
cnames.push_back(kind::kindToString(k));
cargs.push_back( std::vector< CVC4::Type >() );
if( k==kind::NOT ){
- cargs.back().push_back(mkUnresolvedType(ssb.str()));
+ cargs.back().push_back(unres_bt);
}else if( k==kind::AND || k==kind::OR ){
- cargs.back().push_back(mkUnresolvedType(ssb.str()));
- cargs.back().push_back(mkUnresolvedType(ssb.str()));
- }else if( k==kind::EQUAL ){
- cargs.back().push_back(mkUnresolvedType(ss.str()));
- cargs.back().push_back(mkUnresolvedType(ss.str()));
+ cargs.back().push_back(unres_bt);
+ cargs.back().push_back(unres_bt);
}
}
- if( range.isInteger() ){
- CVC4::Kind k = kind::LEQ;
+ //add predicates for types
+ for( unsigned i=0; i<types.size(); i++ ){
+ //add equality per type
+ CVC4::Kind k = kind::EQUAL;
Debug("parser-sygus") << "...add for " << k << std::endl;
ops.back().push_back(getExprManager()->operatorOf(k));
- cnames.push_back(kind::kindToString(k));
+ std::stringstream ss;
+ ss << kind::kindToString(k) << "_" << types[i];
+ cnames.push_back(ss.str());
cargs.push_back( std::vector< CVC4::Type >() );
- cargs.back().push_back(mkUnresolvedType(ss.str()));
- cargs.back().push_back(mkUnresolvedType(ss.str()));
+ cargs.back().push_back(unres_types[i]);
+ cargs.back().push_back(unres_types[i]);
+ //type specific predicates
+ if( types[i].isInteger() ){
+ CVC4::Kind k = kind::LEQ;
+ Debug("parser-sygus") << "...add for " << k << std::endl;
+ ops.back().push_back(getExprManager()->operatorOf(k));
+ cnames.push_back(kind::kindToString(k));
+ cargs.push_back( std::vector< CVC4::Type >() );
+ cargs.back().push_back(unres_types[i]);
+ cargs.back().push_back(unres_types[i]);
+ }
+ }
+ if( range==btype ){
+ startIndex = sorts.size();
}
Debug("parser-sygus") << "...make datatype " << datatypes.back() << std::endl;
- Type btype = getExprManager()->booleanType();
datatypes.back().setSygus( btype, bvl, true, true );
mkSygusDatatype( datatypes.back(), ops.back(), cnames, cargs, unresolved_gterm_sym, sygus_to_builtin );
sorts.push_back( btype );
ops.push_back( getExprManager()->mkConst(bval0) );
BitVector bval1(sz, (unsigned int)1);
ops.push_back( getExprManager()->mkConst(bval1) );
+ }else if( type.isBoolean() ){
+ ops.push_back(getExprManager()->mkConst(true));
+ ops.push_back(getExprManager()->mkConst(false));
}
//TODO : others?
}
+// 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,
+ 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< 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,
+ 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 -
+ if( sgt.d_children.size()==1 && sgt.d_expr==getExprManager()->operatorOf(kind::MINUS) ){
+ sgt.d_expr = getExprManager()->operatorOf(kind::UMINUS);
+ }
+ ops[index].push_back( sgt.d_expr );
+ cnames[index].push_back( sgt.d_name );
+ cargs[index].push_back( std::vector< CVC4::Type >() );
+ for( unsigned i=0; i<sgt.d_children.size(); i++ ){
+ std::stringstream ss;
+ ss << datatypes[index].getName() << "_" << ops[index].size() << "_arg_" << i;
+ std::string sub_dname = ss.str();
+ //add datatype for child
+ Type null_type;
+ pushSygusDatatypeDef( null_type, sub_dname, datatypes, sorts, ops, cnames, cargs, allow_const, unresolved_gterm_sym );
+ 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,
+ 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,
+ 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,
+ sygus_vars, sygus_to_builtin, sygus_to_builtin_expr );
+ }
+ }else if( sgt.d_gterm_type==SygusGTerm::gterm_constant ){
+ if( sgt.getNumChildren()!=0 ){
+ parseError("Bad syntax for Sygus Constant.");
+ }
+ std::vector< Expr > consts;
+ mkSygusConstantsForType( sgt.d_type, consts );
+ Debug("parser-sygus") << "...made " << consts.size() << " constants." << std::endl;
+ for( unsigned i=0; i<consts.size(); i++ ){
+ std::stringstream ss;
+ ss << consts[i];
+ Debug("parser-sygus") << "...add for constant " << ss.str() << std::endl;
+ ops[index].push_back( consts[i] );
+ cnames[index].push_back( ss.str() );
+ cargs[index].push_back( std::vector< CVC4::Type >() );
+ }
+ allow_const[index] = true;
+ }else if( sgt.d_gterm_type==SygusGTerm::gterm_variable || sgt.d_gterm_type==SygusGTerm::gterm_input_variable ){
+ if( sgt.getNumChildren()!=0 ){
+ parseError("Bad syntax for Sygus Variable.");
+ }
+ Debug("parser-sygus") << "...process " << sygus_vars.size() << " variables." << std::endl;
+ for( unsigned i=0; i<sygus_vars.size(); i++ ){
+ if( sygus_vars[i].getType()==sgt.d_type ){
+ std::stringstream ss;
+ ss << sygus_vars[i];
+ Debug("parser-sygus") << "...add for variable " << ss.str() << std::endl;
+ ops[index].push_back( sygus_vars[i] );
+ cnames[index].push_back( ss.str() );
+ cargs[index].push_back( std::vector< CVC4::Type >() );
+ }
+ }
+ }else if( sgt.d_gterm_type==SygusGTerm::gterm_nested_sort ){
+ ret = sgt.d_type;
+ }else if( sgt.d_gterm_type==SygusGTerm::gterm_unresolved ){
+ if( isNested ){
+ if( isUnresolvedType(sgt.d_name) ){
+ ret = getSort(sgt.d_name);
+ }else{
+ //nested, unresolved symbol...fail
+ std::stringstream ss;
+ ss << "Cannot handle nested unresolved symbol " << sgt.d_name << std::endl;
+ parseError(ss.str());
+ }
+ }else{
+ //will resolve when adding constructors
+ unresolved_gterm_sym[index].push_back(sgt.d_name);
+ }
+ }else if( sgt.d_gterm_type==SygusGTerm::gterm_ignore ){
+
+ }
+}
+
bool Smt2::pushSygusDatatypeDef( Type t, std::string& dname,
std::vector< CVC4::Datatype >& datatypes,
std::vector< CVC4::Type>& sorts,
for( unsigned i=0; i<cargs[sub_dt_index][0].size(); i++ ){
std::map< CVC4::Type, CVC4::Expr >::iterator it = sygus_to_builtin_expr.find( cargs[sub_dt_index][0][i] );
if( it==sygus_to_builtin_expr.end() ){
+ if( sygus_to_builtin.find( cargs[sub_dt_index][0][i] )==sygus_to_builtin.end() ){
+ std::stringstream ss;
+ ss << "Missing builtin type for type " << cargs[sub_dt_index][0][i] << "!" << std::endl;
+ ss << "Builtin types are currently : " << std::endl;
+ for( std::map< CVC4::Type, CVC4::Type >::iterator itb = sygus_to_builtin.begin(); itb != sygus_to_builtin.end(); ++itb ){
+ ss << " " << itb->first << " -> " << itb->second << std::endl;
+ }
+ parseError(ss.str());
+ }
Type bt = sygus_to_builtin[cargs[sub_dt_index][0][i]];
Debug("parser-sygus") << ": child " << i << " introduce type elem for " << cargs[sub_dt_index][0][i] << " " << bt << std::endl;
std::stringstream ss;
}
void Smt2::processSygusLetConstructor( std::vector< CVC4::Expr >& let_vars,
- int index, int start_index,
+ int index,
std::vector< CVC4::Datatype >& datatypes,
std::vector< CVC4::Type>& sorts,
std::vector< std::vector<CVC4::Expr> >& ops,
Debug("parser-sygus") << " let var " << i << " : " << let_vars[i] << " " << let_vars[i].getType() << std::endl;
let_define_args.push_back( let_vars[i] );
}
+ /*
Debug("parser-sygus") << "index = " << index << ", start index = " << start_index << ", #Current datatypes = " << datatypes.size() << std::endl;
for( unsigned i=start_index; i<datatypes.size(); i++ ){
Debug("parser-sygus") << " datatype " << i << " : " << datatypes[i].getName() << ", #cons = " << cargs[i].size() << std::endl;
}
}
}
+ */
//last argument is the return, pop
cargs[index][dindex].pop_back();
collectSygusLetArgs( let_body, cargs[index][dindex], let_define_args );
}
}
+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 ) {
+ if( startIndex>0 ){
+ CVC4::Datatype tmp_dt = datatypes[0];
+ Type tmp_sort = sorts[0];
+ std::vector< Expr > tmp_ops;
+ tmp_ops.insert( tmp_ops.end(), ops[0].begin(), ops[0].end() );
+ datatypes[0] = datatypes[startIndex];
+ sorts[0] = sorts[startIndex];
+ ops[0].clear();
+ ops[0].insert( ops[0].end(), ops[startIndex].begin(), ops[startIndex].end() );
+ datatypes[startIndex] = tmp_dt;
+ sorts[startIndex] = tmp_sort;
+ ops[startIndex].clear();
+ ops[startIndex].insert( ops[startIndex].begin(), tmp_ops.begin(), tmp_ops.end() );
+ }else if( startIndex<0 ){
+ std::stringstream ss;
+ ss << "warning: no symbol named Start for synth-fun " << fun << std::endl;
+ warning(ss.str());
+ }
+}
void Smt2::defineSygusFuns() {
// only define each one once
}
Expr apply = getExprManager()->mkExpr(kind::APPLY_UF, applyv);
Debug("parser-sygus") << "...made apply " << apply << std::endl;
+ Debug("parser-sygus") << "--> Define " << fun << " as " << lambda << " " << apply << std::endl;
Command* cmd = new DefineFunctionCommand(fun, lambda, sygusVars, apply);
preemptCommand(cmd);
return assertion;
}
+const void Smt2::getSygusPrimedVars( std::vector<Expr>& vars, bool isPrimed ) {
+ for( unsigned i=0; i<d_sygusVars.size(); i++ ){
+ Expr v = d_sygusVars[i];
+ std::map< Expr, bool >::iterator it = d_sygusVarPrimed.find( v );
+ if( it!=d_sygusVarPrimed.end() ){
+ if( it->second==isPrimed ){
+ vars.push_back( v );
+ }
+ }else{
+ //should never happen
+ }
+ }
+}
}/* CVC4::parser namespace */
}/* CVC4 namespace */
class SExpr;
namespace parser {
-
+
class Smt2 : public Parser {
friend class ParserBuilder;
std::stack< std::map<Expr, std::string> > d_unsatCoreNames;
std::vector<Expr> d_sygusVars, d_sygusConstraints, d_sygusFunSymbols;
std::vector< std::pair<std::string, Expr> > d_sygusFuns;
+ std::map< Expr, bool > d_sygusVarPrimed;
size_t d_nextSygusFun;
protected:
return getExprManager()->mkConst(AbstractValue(Integer(name.substr(1))));
}
- Expr mkSygusVar(const std::string& name, const Type& type) {
- Expr e = mkBoundVar(name, type);
- d_sygusVars.push_back(e);
- return e;
- }
+ Expr mkSygusVar(const std::string& name, const Type& type, bool isPrimed = false);
void mkSygusDefaultGrammar( const Type& range, Expr& bvl, const std::string& fun, std::vector<CVC4::Datatype>& datatypes,
- std::vector<Type>& sorts, std::vector< std::vector<Expr> >& ops, std::vector<Expr> sygus_vars );
+ std::vector<Type>& sorts, std::vector< std::vector<Expr> >& ops, std::vector<Expr> sygus_vars, int& startIndex );
void mkSygusConstantsForType( const Type& type, std::vector<CVC4::Expr>& ops );
+ void 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::string> >& cnames,
+ 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,
+ CVC4::Type& ret, bool isNested = false );
+
static bool pushSygusDatatypeDef( Type t, std::string& dname,
std::vector< CVC4::Datatype >& datatypes,
std::vector< CVC4::Type>& sorts,
std::vector< std::vector< std::vector< CVC4::Type > > >& cargs,
std::vector< bool >& allow_const,
std::vector< std::vector< std::string > >& unresolved_gterm_sym );
-
- Type 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::string> >& cnames,
- 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::Expr >& sygus_to_builtin_expr, Type sub_ret );
-
- void processSygusLetConstructor( std::vector< CVC4::Expr >& let_vars,
- int index, int start_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::map< CVC4::Type, CVC4::Type >& sygus_to_builtin,
- std::map< CVC4::Type, CVC4::Expr >& sygus_to_builtin_expr );
+ void setSygusStartIndex( std::string& fun, int startIndex,
+ std::vector< CVC4::Datatype >& datatypes,
+ std::vector< CVC4::Type>& sorts,
+ std::vector< std::vector<CVC4::Expr> >& ops );
void addSygusFun(const std::string& fun, Expr eval) {
d_sygusFuns.push_back(std::make_pair(fun, eval));
Expr getSygusAssertion( std::vector<DatatypeType>& datatypeTypes, std::vector< std::vector<Expr> >& ops,
std::map<DatatypeType, Expr>& evals, std::vector<Expr>& terms,
Expr eval, const Datatype& dt, size_t i, size_t j );
+
+
void addSygusConstraint(Expr constraint) {
d_sygusConstraints.push_back(constraint);
const std::vector<Expr>& getSygusVars() {
return d_sygusVars;
}
+ const void getSygusPrimedVars( std::vector<Expr>& vars, bool isPrimed );
const std::vector<Expr>& getSygusFunSymbols() {
return d_sygusFunSymbols;
void addSygusDatatypeConstructor( CVC4::Datatype& dt, CVC4::Expr op, std::string& cname, std::vector< CVC4::Type >& cargs,
CVC4::Expr& let_body, std::vector< CVC4::Expr >& let_args, unsigned let_num_input_args );
+ Type 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::string> >& cnames,
+ 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::Expr >& sygus_to_builtin_expr, Type sub_ret );
+
+ void processSygusLetConstructor( std::vector< CVC4::Expr >& let_vars, 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::map< CVC4::Type, CVC4::Type >& sygus_to_builtin,
+ std::map< CVC4::Type, CVC4::Expr >& sygus_to_builtin_expr );
+
void addArithmeticOperators();
void addBitvectorOperators();
// extern void Smt2ParserSetAntlrParser(CVC4::parser::AntlrParser* newAntlrParser);
namespace CVC4 {
-
+
class Command;
class Expr;
class ExprManager;
static void printFpParameterizedOp(std::ostream& out, TNode n) throw();
static void toStreamRational(std::ostream& out, const Rational& r, bool decimal) throw();
-
+
void Smt2Printer::toStream(std::ostream& out, TNode n,
int toDepth, bool types, size_t dag) const throw() {
if(dag != 0) {
break;
case kind::FLOATINGPOINT_TYPE:
out << "(_ FloatingPoint "
- << n.getConst<FloatingPointSize>().exponent() << " "
- << n.getConst<FloatingPointSize>().significand()
- << ")";
+ << n.getConst<FloatingPointSize>().exponent() << " "
+ << n.getConst<FloatingPointSize>().significand()
+ << ")";
break;
case kind::CONST_BITVECTOR: {
const BitVector& bv = n.getConst<BitVector>();
const Integer& x = bv.getValue();
unsigned n = bv.getSize();
- out << "(_ ";
- out << "bv" << x <<" " << n;
- out << ")";
+ if(d_variant == sygus_variant ){
+ out << "#b" << bv.toString();
+ }else{
+ out << "(_ ";
+ out << "bv" << x <<" " << n;
+ out << ")";
+ }
+
// //out << "#b";
// while(n-- > 0) {
case roundTowardNegative : out << "roundTowardNegative"; break;
case roundTowardZero : out << "roundTowardZero"; break;
default :
- Unreachable("Invalid value of rounding mode constant (%d)",n.getConst<RoundingMode>());
+ Unreachable("Invalid value of rounding mode constant (%d)",n.getConst<RoundingMode>());
}
break;
case kind::CONST_BOOLEAN:
break;
case kind::CONST_RATIONAL: {
const Rational& r = n.getConst<Rational>();
- toStreamRational(out, r, false);
+ if(d_variant == sygus_variant ){
+ if(r < 0) {
+ out << "-" << -r;
+ }else{
+ toStreamRational(out, r, false);
+ }
+ }else{
+ toStreamRational(out, r, false);
+ }
// Rational r = n.getConst<Rational>();
// if(r < 0) {
// if(r.isIntegral()) {
case kind::BITVECTOR_SGT: out << "bvsgt "; break;
case kind::BITVECTOR_SGE: out << "bvsge "; break;
case kind::BITVECTOR_TO_NAT: out << "bv2nat "; break;
+ case kind::BITVECTOR_REDOR: out << "bvredor "; break;
+ case kind::BITVECTOR_REDAND: out << "bvredand "; break;
case kind::BITVECTOR_EXTRACT:
case kind::BITVECTOR_REPEAT:
// Special case, in model output integer constants that should be
// Real-sorted are wrapped in a type ascription. Handle that here.
- // Note: This is Tim making a guess about Morgan's Code.
- Assert(n[0].getKind() == kind::CONST_RATIONAL);
- toStreamRational(out, n[0].getConst<Rational>(), true);
+ // Note: This is Tim making a guess about Morgan's Code.
+ Assert(n[0].getKind() == kind::CONST_RATIONAL);
+ toStreamRational(out, n[0].getConst<Rational>(), true);
//toStream(out, n[0], -1, false);
//out << ".0";
-
+
return;
}
out << "(as ";
return;
}
break;
- case kind::APPLY_TESTER:
case kind::APPLY_CONSTRUCTOR:
+ case kind::APPLY_TESTER:
case kind::APPLY_SELECTOR:
case kind::APPLY_SELECTOR_TOTAL:
case kind::PARAMETRIC_DATATYPE:
if( n.getMetaKind() == kind::metakind::PARAMETERIZED &&
stillNeedToPrintParams ) {
if(toDepth != 0) {
- toStream(out, n.getOperator(), toDepth < 0 ? toDepth : toDepth - 1, types);
+ if( d_variant==sygus_variant && n.getKind()==kind::APPLY_CONSTRUCTOR ){
+ std::stringstream ss;
+ toStream(ss, n.getOperator(), toDepth < 0 ? toDepth : toDepth - 1, types);
+ std::string tmp = ss.str();
+ size_t pos = 0;
+ if((pos = tmp.find("__Enum__", pos)) != std::string::npos){
+ tmp.replace(pos, 8, "::");
+ }
+ out << tmp;
+ }else{
+ toStream(out, n.getOperator(), toDepth < 0 ? toDepth : toDepth - 1, types);
+ }
} else {
out << "(...)";
}
case kind::BITVECTOR_PLUS: return "bvadd";
case kind::BITVECTOR_SUB: return "bvsub";
case kind::BITVECTOR_NEG: return "bvneg";
+ case kind::BITVECTOR_UDIV_TOTAL:
case kind::BITVECTOR_UDIV: return "bvudiv";
case kind::BITVECTOR_UREM: return "bvurem";
case kind::BITVECTOR_SDIV: return "bvsdiv";
case kind::BITVECTOR_SLE: return "bvsle";
case kind::BITVECTOR_SGT: return "bvsgt";
case kind::BITVECTOR_SGE: return "bvsge";
+ case kind::BITVECTOR_REDOR: return "bvredor";
+ case kind::BITVECTOR_REDAND: return "bvredand";
case kind::BITVECTOR_EXTRACT: return "extract";
case kind::BITVECTOR_REPEAT: return "repeat";
case kind::FLOATINGPOINT_ISN: return "fp.isNormal";
case kind::FLOATINGPOINT_ISSN: return "fp.isSubnormal";
- case kind::FLOATINGPOINT_ISZ: return "fp.isZero";
+ case kind::FLOATINGPOINT_ISZ: return "fp.isZero";
case kind::FLOATINGPOINT_ISINF: return "fp.isInfinite";
case kind::FLOATINGPOINT_ISNAN: return "fp.isNaN";
case kind::FLOATINGPOINT_ISNEG: return "fp.isNegative";
}
}
} else if(dynamic_cast<const DeclareFunctionCommand*>(c) != NULL) {
- const DeclareFunctionCommand* dfc = (const DeclareFunctionCommand*)c;
+ const DeclareFunctionCommand* dfc = (const DeclareFunctionCommand*)c;
Node n = Node::fromExpr( dfc->getFunction() );
if(dfc->getPrintInModelSetByUser()) {
if(!dfc->getPrintInModel()) {
out << "(define-fun " << n << " () "
<< n.getType() << " ";
if(val.getType().isInteger() && n.getType().isReal() && !n.getType().isInteger()) {
- //toStreamReal(out, val, true);
- toStreamRational(out, val.getConst<Rational>(), true);
- //out << val << ".0";
+ //toStreamReal(out, val, true);
+ toStreamRational(out, val.getConst<Rational>(), true);
+ //out << val << ".0";
} else {
out << val;
}
static void toStreamRational(std::ostream& out, const Rational& r, bool decimal) throw() {
bool neg = r.sgn() < 0;
-
+
// TODO:
// We are currently printing (- (/ 5 3))
// instead of (/ (- 5) 3) which is what is in the SMT-LIB value in the theory definition.
// Before switching, I'll keep to what was there and send an email.
// Tim: Apologies for the ifs on one line but in this case they are cleaner.
-
+
if (neg) { out << "(- "; }
-
+
if(r.isIntegral()) {
if (neg) {
out << (-r);
operator BITVECTOR_SGT 2 "bit-vector signed greater than (the two bit-vector parameters must have same width)"
operator BITVECTOR_SGE 2 "bit-vector signed greater than or equal (the two bit-vector parameters must have same width)"
+operator BITVECTOR_REDOR 1 "bit-vector redor"
+operator BITVECTOR_REDAND 1 "bit-vector redand"
+
operator BITVECTOR_EAGER_ATOM 1 "formula to be treated as a bv atom via eager bit-blasting (internal-only symbol)"
operator BITVECTOR_ACKERMANIZE_UDIV 1 "term to be treated as a variable; used for eager bit-blasting Ackermann expansion of bvudiv (internal-only symbol)"
operator BITVECTOR_ACKERMANIZE_UREM 1 "term to be treated as a variable; used for eager bit-blasting Ackermann expansion of bvurem (internal-only symbol)"
typerule BITVECTOR_SGT ::CVC4::theory::bv::BitVectorPredicateTypeRule
typerule BITVECTOR_SGE ::CVC4::theory::bv::BitVectorPredicateTypeRule
+typerule BITVECTOR_REDOR ::CVC4::theory::bv::BitVectorUnaryPredicateTypeRule
+typerule BITVECTOR_REDAND ::CVC4::theory::bv::BitVectorUnaryPredicateTypeRule
+
+
typerule BITVECTOR_EAGER_ATOM ::CVC4::theory::bv::BitVectorEagerAtomTypeRule
typerule BITVECTOR_ACKERMANIZE_UDIV ::CVC4::theory::bv::BitVectorAckermanizationUdivTypeRule
typerule BITVECTOR_ACKERMANIZE_UREM ::CVC4::theory::bv::BitVectorAckermanizationUremTypeRule
UgeEliminate,
SgeEliminate,
SgtEliminate,
+ RedorEliminate,
+ RedandEliminate,
SubEliminate,
SltEliminate,
SleEliminate,
case SgtEliminate: out << "SgtEliminate"; return out;
case UgeEliminate: out << "UgeEliminate"; return out;
case SgeEliminate: out << "SgeEliminate"; return out;
+ case RedorEliminate: out << "RedorEliminate"; return out;
+ case RedandEliminate: out << "RedandEliminate"; return out;
case RepeatEliminate: out << "RepeatEliminate"; return out;
case RotateLeftEliminate: out << "RotateLeftEliminate"; return out;
case RotateRightEliminate:out << "RotateRightEliminate";return out;
RewriteRule<UltPlusOne> rule119;
RewriteRule<ConcatToMult> rule120;
RewriteRule<IsPowerOfTwo> rule121;
+ RewriteRule<RedorEliminate> rule122;
+ RewriteRule<RedandEliminate> rule123;
};
template<> inline
return utils::mkConcat(extension, node[0]);
}
+template<>
+bool RewriteRule<RedorEliminate>::applies(TNode node) {
+ return (node.getKind() == kind::BITVECTOR_REDOR);
+}
+
+template<>
+Node RewriteRule<RedorEliminate>::apply(TNode node) {
+ Debug("bv-rewrite") << "RewriteRule<RedorEliminate>(" << node << ")" << std::endl;
+ TNode a = node[0];
+ unsigned size = utils::getSize(node[0]);
+ Node result = NodeManager::currentNM()->mkNode(kind::EQUAL, a, utils::mkConst( size, 0 ) );
+ return result.negate();
+}
+
+template<>
+bool RewriteRule<RedandEliminate>::applies(TNode node) {
+ return (node.getKind() == kind::BITVECTOR_REDAND);
+}
+
+template<>
+Node RewriteRule<RedandEliminate>::apply(TNode node) {
+ Debug("bv-rewrite") << "RewriteRule<RedandEliminate>(" << node << ")" << std::endl;
+ TNode a = node[0];
+ unsigned size = utils::getSize(node[0]);
+ Node result = NodeManager::currentNM()->mkNode(kind::EQUAL, a, utils::mkOnes( size ) );
+ return result;
+}
}
}
return RewriteResponse(REWRITE_AGAIN_FULL, resultNode);
}
+RewriteResponse TheoryBVRewriter::RewriteRedor(TNode node, bool prerewrite){
+ Node resultNode = LinearRewriteStrategy
+ < RewriteRule<RedorEliminate>
+ >::apply(node);
+
+ return RewriteResponse(REWRITE_AGAIN_FULL, resultNode);
+}
+
+RewriteResponse TheoryBVRewriter::RewriteRedand(TNode node, bool prerewrite){
+ Node resultNode = LinearRewriteStrategy
+ < RewriteRule<RedandEliminate>
+ >::apply(node);
+
+ return RewriteResponse(REWRITE_AGAIN_FULL, resultNode);
+}
+
RewriteResponse TheoryBVRewriter::RewriteBVToNat(TNode node, bool prerewrite) {
Node resultNode = LinearRewriteStrategy
< RewriteRule<BVToNatEliminate>
d_rewriteTable [ kind::BITVECTOR_SIGN_EXTEND ] = RewriteSignExtend;
d_rewriteTable [ kind::BITVECTOR_ROTATE_RIGHT ] = RewriteRotateRight;
d_rewriteTable [ kind::BITVECTOR_ROTATE_LEFT ] = RewriteRotateLeft;
+ d_rewriteTable [ kind::BITVECTOR_REDOR ] = RewriteRedor;
+ d_rewriteTable [ kind::BITVECTOR_REDAND ] = RewriteRedand;
d_rewriteTable [ kind::BITVECTOR_TO_NAT ] = RewriteBVToNat;
d_rewriteTable [ kind::INT_TO_BITVECTOR ] = RewriteIntToBV;
static RewriteResponse RewriteSignExtend(TNode node, bool prerewrite = false);
static RewriteResponse RewriteRotateRight(TNode node, bool prerewrite = false);
static RewriteResponse RewriteRotateLeft(TNode node, bool prerewrite = false);
+ static RewriteResponse RewriteRedor(TNode node, bool prerewrite = false);
+ static RewriteResponse RewriteRedand(TNode node, bool prerewrite = false);
static RewriteResponse RewriteBVToNat(TNode node, bool prerewrite = false);
static RewriteResponse RewriteIntToBV(TNode node, bool prerewrite = false);
}
};/* class BitVectorPredicateTypeRule */
+class BitVectorUnaryPredicateTypeRule {
+public:
+ inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check)
+ throw (TypeCheckingExceptionPrivate, AssertionException) {
+ if( check ) {
+ TypeNode type = n[0].getType(check);
+ if (!type.isBitVector()) {
+ throw TypeCheckingExceptionPrivate(n, "expecting bit-vector terms");
+ }
+ }
+ return nodeManager->booleanType();
+ }
+};/* class BitVectorUnaryPredicateTypeRule */
+
class BitVectorEagerAtomTypeRule {
public:
inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check)
node.getKind() == kind::BITVECTOR_SGE ||
node.getKind() == kind::BITVECTOR_ULE ||
node.getKind() == kind::BITVECTOR_SLE ||
+ node.getKind() == kind::BITVECTOR_REDOR ||
+ node.getKind() == kind::BITVECTOR_REDAND ||
( node.getKind() == kind::NOT && (node[0].getKind() == kind::EQUAL ||
node[0].getKind() == kind::BITVECTOR_ULT ||
node[0].getKind() == kind::BITVECTOR_SLT ||
node[0].getKind() == kind::BITVECTOR_SGT ||
node[0].getKind() == kind::BITVECTOR_SGE ||
node[0].getKind() == kind::BITVECTOR_ULE ||
- node[0].getKind() == kind::BITVECTOR_SLE)))
+ node[0].getKind() == kind::BITVECTOR_SLE ||
+ node[0].getKind() == kind::BITVECTOR_REDOR ||
+ node[0].getKind() == kind::BITVECTOR_REDAND)))
{
return true;
}
std::map< Node, ProgSearch * >::iterator it = d_prog_search.find( a );
ProgSearch * ps;
if( it==d_prog_search.end() ){
- ps = new ProgSearch( this, a, d_context );
+ //check if sygus type
+ TypeNode tn = a.getType();
+ Assert( DatatypesRewriter::isTypeDatatype( tn ) );
+ const Datatype& dt = ((DatatypeType)(tn).toType()).getDatatype();
+ if( dt.isSygus() ){
+ ps = new ProgSearch( this, a, d_context );
+ }else{
+ ps = NULL;
+ }
d_prog_search[a] = ps;
}else{
ps = it->second;
}
- ps->addTester( tst );
+ if( ps ){
+ ps->addTester( tst );
+ }
}
}
Node SygusSymBreak::ProgSearch::getCandidateProgramAtDepth( int depth, Node prog, int curr_depth, Node parent, std::map< TypeNode, int >& var_count,
std::vector< Node >& testers, std::map< Node, std::vector< Node > >& testers_u ) {
Assert( depth>=curr_depth );
- Trace("sygus-sym-break-debug") << "Reconstructing program for " << prog << " at depth " << curr_depth << "/" << depth << std::endl;
+ Trace("sygus-sym-break-debug") << "Reconstructing program for " << prog << " at depth " << curr_depth << "/" << depth << " " << prog.getType() << std::endl;
NodeMap::const_iterator it = d_testers.find( prog );
if( it!=d_testers.end() ){
Node tst = (*it).second;
int tsize = d_tds->getSygusTermSize( prog );
if( itnp==d_normalized_to_orig[at].end() ){
d_normalized_to_orig[at][progr] = prog;
- if( progr.getKind()==SKOLEM && d_tds->getSygusType( progr )==at ){
+ if( progr.getKind()==SKOLEM && d_tds->getSygusTypeForVar( progr )==at ){
Trace("sygus-nf") << "* Sygus sym break : " << prog << " rewrites to variable " << progr << " of same type as self" << std::endl;
d_redundant[at][prog] = true;
red = true;
}
void CegConjecture::initializeGuard( QuantifiersEngine * qe ){
- if( d_guard.isNull() ){
+ if( isAssigned() && d_guard.isNull() ){
d_guard = Rewriter::rewrite( NodeManager::currentNM()->mkSkolem( "G", NodeManager::currentNM()->booleanType() ) );
//specify guard behavior
d_guard = qe->getValuation().ensureLiteral( d_guard );
return d_ceg_si->isSingleInvocation();
}
+bool CegConjecture::needsCheck() {
+ return d_active && !d_infeasible && ( !isSingleInvocation() || d_ceg_si->needsCheck() );
+}
+
CegInstantiation::CegInstantiation( QuantifiersEngine * qe, context::Context* c ) : QuantifiersModule( qe ){
d_conj = new CegConjecture( qe->getSatContext() );
d_last_inst_si = false;
Trace("cegqi-engine") << "---Counterexample Guided Instantiation Engine---" << std::endl;
Trace("cegqi-engine-debug") << std::endl;
Trace("cegqi-engine-debug") << "Current conjecture status : active : " << d_conj->d_active << " feasible : " << !d_conj->d_infeasible << std::endl;
- if( d_conj->d_active && !d_conj->d_infeasible ){
+ if( d_conj->needsCheck() ){
checkCegConjecture( d_conj );
}
Trace("cegqi-engine") << "Finished Counterexample Guided Instantiation engine." << std::endl;
}
Node CegInstantiation::getNextDecisionRequest() {
- d_conj->initializeGuard( d_quantEngine );
- bool value;
- if( !d_quantEngine->getValuation().hasSatValue( d_conj->d_guard, value ) ) {
- //if( d_conj->d_guard_split.isNull() ){
- // Node lem = NodeManager::currentNM()->mkNode( OR, d_conj->d_guard.negate(), d_conj->d_guard );
- // d_quantEngine->getOutputChannel().lemma( lem );
- //}
- Trace("cegqi-debug") << "CEGQI : Decide next on : " << d_conj->d_guard << "..." << std::endl;
- return d_conj->d_guard;
- }
//enforce fairness
- if( d_conj->isAssigned() && 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 ) ) {
- if( !value ){
- d_conj->d_curr_lit.set( d_conj->d_curr_lit.get() + 1 );
- lit = d_conj->getLiteral( d_quantEngine, d_conj->d_curr_lit.get() );
- Trace("cegqi-debug") << "CEGQI : Decide on next lit : " << lit << "..." << std::endl;
+ if( d_conj->isAssigned() ){
+ d_conj->initializeGuard( d_quantEngine );
+ bool value;
+ if( !d_quantEngine->getValuation().hasSatValue( d_conj->d_guard, value ) ) {
+ //if( d_conj->d_guard_split.isNull() ){
+ // Node lem = NodeManager::currentNM()->mkNode( OR, d_conj->d_guard.negate(), d_conj->d_guard );
+ // d_quantEngine->getOutputChannel().lemma( lem );
+ //}
+ 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 ) ) {
+ if( !value ){
+ d_conj->d_curr_lit.set( d_conj->d_curr_lit.get() + 1 );
+ lit = d_conj->getLiteral( d_quantEngine, d_conj->d_curr_lit.get() );
+ Trace("cegqi-debug") << "CEGQI : Decide on next lit : " << lit << "..." << std::endl;
+ return lit;
+ }
+ }else{
+ Trace("cegqi-debug") << "CEGQI : Decide on current lit : " << lit << "..." << std::endl;
return lit;
}
- }else{
- Trace("cegqi-debug") << "CEGQI : Decide on current lit : " << lit << "..." << std::endl;
- return lit;
}
}
}
void CegInstantiation::printSynthSolution( std::ostream& out ) {
- if( d_conj ){
+ if( d_conj->isAssigned() ){
+ Trace("cegqi-debug") << "Printing synth solution..." << std::endl;
//if( !(Trace.isOn("cegqi-stats")) ){
// out << "Solution:" << std::endl;
//}
out << ")" << std::endl;
}
}
+ }else{
+ Assert( false );
}
}
CegqiFairMode getCegqiFairMode();
/** is single invocation */
bool isSingleInvocation();
+ /** needs check */
+ bool needsCheck();
};
d_sol = NULL;
d_c_inst_match_trie = NULL;
d_cinst = NULL;
+ d_has_ites = true;
}
Node CegConjectureSingleInv::getSingleInvLemma( Node guard ) {
if( !d_single_inv.isNull() ) {
- Assert( d_single_inv.getKind()==FORALL );
d_single_inv_var.clear();
d_single_inv_sk.clear();
- for( unsigned i=0; i<d_single_inv[0].getNumChildren(); i++ ){
- std::stringstream ss;
- ss << "k_" << d_single_inv[0][i];
- Node k = NodeManager::currentNM()->mkSkolem( ss.str(), d_single_inv[0][i].getType(), "single invocation function skolem" );
- d_single_inv_var.push_back( d_single_inv[0][i] );
- d_single_inv_sk.push_back( k );
- d_single_inv_sk_index[k] = i;
+ Node inst;
+ if( d_single_inv.getKind()==FORALL ){
+ for( unsigned i=0; i<d_single_inv[0].getNumChildren(); i++ ){
+ std::stringstream ss;
+ ss << "k_" << d_single_inv[0][i];
+ Node k = NodeManager::currentNM()->mkSkolem( ss.str(), d_single_inv[0][i].getType(), "single invocation function skolem" );
+ d_single_inv_var.push_back( d_single_inv[0][i] );
+ d_single_inv_sk.push_back( k );
+ d_single_inv_sk_index[k] = i;
+ }
+ inst = d_single_inv[1].substitute( d_single_inv_var.begin(), d_single_inv_var.end(), d_single_inv_sk.begin(), d_single_inv_sk.end() );
+ }else{
+ inst = d_single_inv;
}
- Node inst = d_single_inv[1].substitute( d_single_inv_var.begin(), d_single_inv_var.end(), d_single_inv_sk.begin(), d_single_inv_sk.end() );
inst = TermDb::simpleNegate( inst );
Trace("cegqi-si") << "Single invocation initial lemma : " << inst << std::endl;
//initialize the instantiator for this
- CegqiOutputSingleInv * cosi = new CegqiOutputSingleInv( this );
- d_cinst = new CegInstantiator( d_qe, cosi );
- d_cinst->d_vars.insert( d_cinst->d_vars.end(), d_single_inv_sk.begin(), d_single_inv_sk.end() );
+ if( !d_single_inv_sk.empty() ){
+ CegqiOutputSingleInv * cosi = new CegqiOutputSingleInv( this );
+ d_cinst = new CegInstantiator( d_qe, cosi );
+ d_cinst->d_vars.insert( d_cinst->d_vars.end(), d_single_inv_sk.begin(), d_single_inv_sk.end() );
+ }else{
+ d_cinst = NULL;
+ }
return NodeManager::currentNM()->mkNode( OR, guard.negate(), inst );
}else{
std::map< Node, std::map< Node, bool > > contains;
for( unsigned i=0; i<q[0].getNumChildren(); i++ ){
progs.push_back( q[0][i] );
+ //check whether all types have ITE
+ TypeNode tn = q[0][i].getType();
+ d_qe->getTermDatabaseSygus()->registerSygusType( tn );
+ if( !d_qe->getTermDatabaseSygus()->sygusToBuiltinType( tn ).isBoolean() ){
+ if( !d_qe->getTermDatabaseSygus()->hasKind( tn, ITE ) ){
+ d_has_ites = false;
+ }
+ }
}
//collect information about conjunctions
bool singleInvocation = false;
//construct the single invocation version of the property
Trace("cegqi-si") << "Single invocation formula conjuncts are : " << std::endl;
//std::vector< Node > si_conj;
- Assert( !pbvs.empty() );
- Node pbvl = NodeManager::currentNM()->mkNode( BOUND_VAR_LIST, pbvs );
+ Node pbvl;
+ if( !pbvs.empty() ){
+ pbvl = NodeManager::currentNM()->mkNode( BOUND_VAR_LIST, pbvs );
+ }
for( std::map< Node, std::vector< Node > >::iterator it = children.begin(); it != children.end(); ++it ){
//should hold since we prevent miniscoping
Assert( d_single_inv.isNull() );
if( singleInvocation ){
Node bd = conjuncts.size()==1 ? conjuncts[0] : NodeManager::currentNM()->mkNode( OR, conjuncts );
- d_single_inv = NodeManager::currentNM()->mkNode( FORALL, pbvl, bd );
+ 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.wasSetByUser() ){
+ /*
+ if( options::eMatching() && options::eMatching.wasSetByUser() ){
Node bd = d_qe->getTermDatabase()->getInstConstantBody( d_single_inv );
std::vector< Node > patTerms;
std::vector< Node > exclude;
}
}
}
+ */
}
}
}
if( !singleInvocation ){
Trace("cegqi-si") << "Property is not single invocation." << std::endl;
if( options::cegqiSingleInvAbort() ){
- Message() << "Property is not single invocation." << std::endl;
+ Notice() << "Property is not single invocation." << std::endl;
exit( 0 );
}
+ }else{
+ if( options::cegqiSingleInvPreRegInst() && d_single_inv.getKind()==FORALL ){
+ Trace("cegqi-si-presolve") << "Check " << d_single_inv << std::endl;
+ //at preregister time, add proxy of obvious instantiations up front, which helps learning during preprocessing
+ std::vector< Node > vars;
+ std::map< Node, std::vector< Node > > teq;
+ for( unsigned i=0; i<d_single_inv[0].getNumChildren(); i++ ){
+ vars.push_back( d_single_inv[0][i] );
+ teq[d_single_inv[0][i]].clear();
+ }
+ collectPresolveEqTerms( d_single_inv[1], teq );
+ std::vector< Node > terms;
+ std::vector< Node > conj;
+ getPresolveEqConjuncts( vars, terms, teq, d_single_inv, conj );
+
+ if( !conj.empty() ){
+ Node lem = conj.size()==1 ? conj[0] : NodeManager::currentNM()->mkNode( AND, conj );
+ Node g = NodeManager::currentNM()->mkSkolem( "g", NodeManager::currentNM()->booleanType() );
+ lem = NodeManager::currentNM()->mkNode( OR, g, lem );
+ d_qe->getOutputChannel().lemma( lem, false, true );
+ }
+ }
+ }
+}
+
+void CegConjectureSingleInv::collectPresolveEqTerms( Node n, std::map< Node, std::vector< Node > >& teq ) {
+ if( n.getKind()==EQUAL ){
+ for( unsigned i=0; i<2; i++ ){
+ std::map< Node, std::vector< Node > >::iterator it = teq.find( n[i] );
+ if( it!=teq.end() ){
+ Node nn = n[ i==0 ? 1 : 0 ];
+ if( std::find( it->second.begin(), it->second.end(), nn )==it->second.end() ){
+ it->second.push_back( nn );
+ Trace("cegqi-si-presolve") << " - " << n[i] << " = " << nn << std::endl;
+ }
+ }
+ }
+ }
+ for( unsigned i=0; i<n.getNumChildren(); i++ ){
+ collectPresolveEqTerms( n[i], teq );
+ }
+}
+
+void CegConjectureSingleInv::getPresolveEqConjuncts( std::vector< Node >& vars, std::vector< Node >& terms,
+ std::map< Node, std::vector< Node > >& teq, Node f, std::vector< Node >& conj ) {
+ if( conj.size()<1000 ){
+ if( terms.size()==f[0].getNumChildren() ){
+ Node c = f[1].substitute( vars.begin(), vars.end(), terms.begin(), terms.end() );
+ conj.push_back( c );
+ }else{
+ unsigned i = terms.size();
+ Node v = f[0][i];
+ terms.push_back( Node::null() );
+ for( unsigned j=0; j<teq[v].size(); j++ ){
+ terms[i] = teq[v][j];
+ getPresolveEqConjuncts( vars, terms, teq, f, conj );
+ }
+ terms.pop_back();
+ }
}
}
}
void CegConjectureSingleInv::check( std::vector< Node >& lems ) {
- if( !d_single_inv.isNull() ) {
- Assert( d_cinst!=NULL );
+ if( !d_single_inv.isNull() && d_cinst!=NULL ) {
d_curr_lemmas.clear();
//check if there are delta lemmas
d_cinst->getDeltaLemmas( lems );
}
}
-Node CegConjectureSingleInv::constructSolution( unsigned i, unsigned index ) {
+Node CegConjectureSingleInv::constructSolution( std::vector< unsigned >& indices, unsigned i, unsigned index ) {
Assert( index<d_inst.size() );
Assert( i<d_inst[index].size() );
+ unsigned uindex = indices[index];
if( index==d_inst.size()-1 ){
- return d_inst[index][i];
+ return d_inst[uindex][i];
}else{
- Node cond = d_lemmas_produced[index];
+ Node cond = d_lemmas_produced[uindex];
cond = TermDb::simpleNegate( cond );
- Node ite1 = d_inst[index][i];
- Node ite2 = constructSolution( i, index+1 );
+ Node ite1 = d_inst[uindex][i];
+ Node ite2 = constructSolution( indices, i, index+1 );
return NodeManager::currentNM()->mkNode( ITE, cond, ite1, ite2 );
}
}
+//TODO: use term size?
+struct sortSiInstanceIndices {
+ CegConjectureSingleInv* d_ccsi;
+ int d_i;
+ bool operator() (unsigned i, unsigned j) {
+ if( d_ccsi->d_inst[i][d_i].isConst() && !d_ccsi->d_inst[j][d_i].isConst() ){
+ return true;
+ }else{
+ return false;
+ }
+ }
+};
+
+/*
+Node removeBooleanIte( Node n ){
+ if( n.getKind()==ITE && n.getType().isBoolean() ){
+ Node n1 = removeBooleanIte( n[1] );
+ Node n2 = removeBooleanIte( n[2] );
+ return NodeManager::currentNM()->mkNode( OR, NodeManager::currentNM()->mkNode( AND, n[0], n1 ),
+ NodeManager::currentNM()->mkNode( AND, n[0].negate(), n2 ) );
+ }else{
+ bool childChanged = false;
+ std::vector< Node > children;
+ for( unsigned i=0; i<n.getNumChildren(); i++ ){
+ Node nn = removeBooleanIte( n[i] );
+ children.push_back( nn );
+ childChanged = childChanged || nn!=n[i];
+ }
+ if( childChanged ){
+ if( n.hasOperator() ){
+ children.insert( children.begin(), n.getOperator() );
+ }
+ return NodeManager::currentNM()->mkNode( n.getKind(), children );
+ }else{
+ return n;
+ }
+ }
+}
+*/
+
Node CegConjectureSingleInv::getSolution( unsigned sol_index, TypeNode stn, int& reconstructed ){
Assert( d_sol!=NULL );
Assert( !d_lemmas_produced.empty() );
d_sol->d_varList.push_back( varList[i-1] );
}
//construct the solution
- Node s = constructSolution( sol_index, 0 );
+ Trace("csi-sol") << "Sort solution return values " << sol_index << std::endl;
+ Assert( d_lemmas_produced.size()==d_inst.size() );
+ std::vector< unsigned > indices;
+ for( unsigned i=0; i<d_lemmas_produced.size(); i++ ){
+ Assert( sol_index<d_inst[i].size() );
+ indices.push_back( i );
+ }
+ //sort indices based on heuristic : currently, do all constant returns first (leads to simpler conditions)
+ // TODO : to minimize solution size, put the largest term last
+ sortSiInstanceIndices ssii;
+ ssii.d_ccsi = this;
+ ssii.d_i = sol_index;
+ std::sort( indices.begin(), indices.end(), ssii );
+ Trace("csi-sol") << "Construct solution" << std::endl;
+ Node s = constructSolution( indices, sol_index, 0 );
s = s.substitute( vars.begin(), vars.end(), d_varList.begin(), d_varList.end() );
d_orig_solution = s;
if( reconstructed==1 ){
Trace("csi-sol") << "Solution (post-reconstruction into Sygus): " << d_sygus_solution << std::endl;
}
+ }else{
+ ////remove boolean ITE (not allowed for sygus comp 2015)
+ //d_solution = removeBooleanIte( d_solution );
+ //Trace("csi-sol") << "Solution (after remove boolean ITE) : " << d_solution << std::endl;
}
}
}
+bool CegConjectureSingleInv::needsCheck() {
+ if( options::cegqiSingleInvMultiInstAbort() ){
+ if( !hasITEs() ){
+ return d_inst.empty();
+ }
+ }
+ 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 );
+ //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 );
//constructing solution
- Node constructSolution( unsigned i, unsigned index );
+ Node constructSolution( std::vector< unsigned >& indices, unsigned i, unsigned index );
private:
//map from programs to variables in single invocation property
std::map< Node, Node > d_single_inv_map;
//list of skolems for each program
std::vector< Node > d_single_inv_var;
//lemmas produced
- std::vector< Node > d_lemmas_produced;
- std::vector< std::vector< Node > > d_inst;
inst::InstMatchTrie d_inst_match_trie;
inst::CDInstMatchTrie * d_c_inst_match_trie;
// solution
Node d_orig_solution;
Node d_solution;
Node d_sygus_solution;
+ bool d_has_ites;
+public:
+ //lemmas produced
+ std::vector< Node > d_lemmas_produced;
+ std::vector< std::vector< Node > > d_inst;
private:
std::vector< Node > d_curr_lemmas;
//add instantiation
void check( std::vector< Node >& lems );
//get solution
Node getSolution( unsigned sol_index, TypeNode stn, int& reconstructed );
+ // has ites
+ bool hasITEs() { return d_has_ites; }
// is single invocation
bool isSingleInvocation() { return !d_single_inv.isNull(); }
+ //needs check
+ bool needsCheck();
};
}
Trace("csi-sol-debug") << "For " << s << ", can pull " << cond << " -> " << t << " with remainder " << rem << std::endl;
t = pullITEs( t );
rem = pullITEs( rem );
+ Trace("csi-pull-ite") << "PI: Rewrite : " << s << std::endl;
+ Node prev = s;
s = NodeManager::currentNM()->mkNode( ITE, TermDb::simpleNegate( cond ), t, rem );
- //Trace("csi-debug-sol") << "Now : " << s << std::endl;
+ Trace("csi-pull-ite") << "PI: Rewrite Now : " << s << std::endl;
+ Trace("csi-pull-ite") << "(= " << prev << " " << s << ")" << std::endl;
success = true;
}
}while( success );
bool CegConjectureSingleInvSol::pullITECondition( Node root, Node n_ite, std::vector< Node >& conj, Node& t, Node& rem, int depth ) {
Assert( n_ite.getKind()==ITE );
std::vector< Node > curr_conj;
+ std::vector< Node > orig_conj;
bool isAnd;
if( n_ite[0].getKind()==AND || n_ite[0].getKind()==OR ){
isAnd = n_ite[0].getKind()==AND;
for( unsigned i=0; i<n_ite[0].getNumChildren(); i++ ){
Node cond = n_ite[0][i];
+ orig_conj.push_back( cond );
if( n_ite[0].getKind()==OR ){
cond = TermDb::simpleNegate( cond );
}
}else{
Node neg = n_ite[0].negate();
if( std::find( conj.begin(), conj.end(), neg )!=conj.end() ){
+ //if negation of condition exists, use it
isAnd = false;
curr_conj.push_back( neg );
}else{
+ //otherwise, use condition
isAnd = true;
curr_conj.push_back( n_ite[0] );
}
+ orig_conj.push_back( n_ite[0] );
}
// take intersection with current conditions
std::vector< Node > new_conj;
//make remainder : strip out conditions in conj
Assert( !conj.empty() );
std::vector< Node > cond_c;
+ Assert( orig_conj.size()==curr_conj.size() );
for( unsigned i=0; i<curr_conj.size(); i++ ){
if( std::find( conj.begin(), conj.end(), curr_conj[i] )==conj.end() ){
- cond_c.push_back( curr_conj[i] );
+ cond_c.push_back( orig_conj[i] );
}
}
if( cond_c.empty() ){
- rem = isAnd ? tval : rem;
+ rem = tval;
}else{
Node new_cond = cond_c.size()==1 ? cond_c[0] : NodeManager::currentNM()->mkNode( n_ite[0].getKind(), cond_c );
rem = NodeManager::currentNM()->mkNode( ITE, new_cond, isAnd ? tval : rem, isAnd ? rem : tval );
ret = NodeManager::currentNM()->mkNode( ITE, exp_c, ret[1], ret[2] );
}
if( !d_qe->getTermDatabaseSygus()->hasKind( stnc[0], ret[0].getKind() ) ){
- Trace("csi-sol") << "Flatten based on " << ret[0] << "." << std::endl;
+ Trace("csi-simp-debug") << "Flatten based on " << ret[0] << "." << std::endl;
ret = flattenITEs( ret, false );
}
}
}
if( !new_vars.empty() ){
if( !inc.empty() ){
- Node ret = inc.size()==1 ? sol[0] : NodeManager::currentNM()->mkNode( sol.getKind(), inc );
+ Node ret = inc.size()==1 ? inc[0] : NodeManager::currentNM()->mkNode( sol.getKind(), inc );
Trace("csi-simp") << "Base return is : " << ret << std::endl;
// apply substitution
ret = ret.substitute( new_vars.begin(), new_vars.end(), new_subs.begin(), new_subs.end() );
}
}while( !new_t.isNull() );
}
+ //get decompositions
for( unsigned i=0; i<dt.getNumConstructors(); i++ ){
Kind k = d_qe->getTermDatabaseSygus()->getArgKind( stn, i );
- if( k==AND || k==OR ){
- equiv.push_back( NodeManager::currentNM()->mkNode( k, min_t, min_t ) );
- equiv.push_back( NodeManager::currentNM()->mkNode( k, min_t, NodeManager::currentNM()->mkConst( k==AND ) ) );
- }
+ getEquivalentTerms( k, min_t, equiv );
}
//assign ids to terms
Trace("csi-rcons-debug") << "Term " << id << " is equivalent to " << equiv.size() << " terms : " << std::endl;
}
}
+void CegConjectureSingleInvSol::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!=d_qe->getTermDatabase()->d_true ){
+ 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 ) );
+ }
+ }
+}
+
}
bool collectReconstructNodes( int pid, std::vector< Node >& ts, const DatatypeConstructor& 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 );
public:
Node reconstructSolution( Node sol, TypeNode stn, int& reconstructed );
public:
--- /dev/null
+/********************* */
+/*! \file fun_def_process.cpp
+ ** \verbatim
+ ** Original author: Andrew Reynolds
+ ** Major contributors: none
+ ** Minor contributors (to current version): none
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2014 New York University and The University of Iowa
+ ** See the file COPYING in the top-level source directory for licensing
+ ** information.\endverbatim
+ **
+ ** This class implements specialized techniques for (recursively) defined functions
+ **/
+
+#include <vector>
+
+#include "theory/quantifiers/fun_def_engine.h"
+#include "theory/rewriter.h"
+#include "theory/quantifiers/term_database.h"
+
+using namespace CVC4;
+using namespace std;
+using namespace CVC4::theory;
+using namespace CVC4::theory::quantifiers;
+using namespace CVC4::kind;
+
+FunDefEngine::FunDefEngine( QuantifiersEngine * qe, context::Context* c ) : QuantifiersModule( qe ) {
+
+}
+
+/* whether this module needs to check this round */
+bool FunDefEngine::needsCheck( Theory::Effort e ) {
+ return e>=Theory::EFFORT_LAST_CALL;
+}
+
+/* reset at a round */
+void FunDefEngine::reset_round( Theory::Effort e ){
+ //TODO
+}
+
+/* Call during quantifier engine's check */
+void FunDefEngine::check( Theory::Effort e, unsigned quant_e ) {
+ //TODO
+}
+
+/* Called for new quantifiers */
+void FunDefEngine::registerQuantifier( Node q ) {
+ //TODO
+}
+
+/** called for everything that gets asserted */
+void FunDefEngine::assertNode( Node n ) {
+ //TODO
+}
--- /dev/null
+/********************* */
+/*! \file fun_def_engine.h
+ ** \verbatim
+ ** Original author: Andrew Reynolds
+ ** Major contributors: none
+ ** Minor contributors (to current version): none
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2014 New York University and The University of Iowa
+ ** See the file COPYING in the top-level source directory for licensing
+ ** information.\endverbatim
+ **
+ ** \brief Specialized techniques for (recursively) defined functions
+ **/
+
+#include "cvc4_private.h"
+
+#ifndef __CVC4__QUANTIFIERS_FUN_DEF_ENGINE_H
+#define __CVC4__QUANTIFIERS_FUN_DEF_ENGINE_H
+
+#include <iostream>
+#include <string>
+#include <vector>
+#include <map>
+#include "expr/node.h"
+#include "expr/type_node.h"
+#include "theory/quantifiers_engine.h"
+
+namespace CVC4 {
+namespace theory {
+namespace quantifiers {
+
+//module for handling (recursively) defined functions
+class FunDefEngine : public QuantifiersModule {
+private:
+
+public:
+ FunDefEngine( QuantifiersEngine * qe, context::Context* c );
+ ~FunDefEngine(){}
+
+ /* whether this module needs to check this round */
+ bool needsCheck( Theory::Effort e );
+ /* reset at a round */
+ void reset_round( Theory::Effort e );
+ /* Call during quantifier engine's check */
+ void check( Theory::Effort e, unsigned quant_e );
+ /* Called for new quantifiers */
+ void registerQuantifier( Node q );
+ /** called for everything that gets asserted */
+ void assertNode( Node n );
+ /** Identify this module (for debugging, dynamic configuration, etc..) */
+ std::string identify() const { return "FunDefEngine"; }
+};
+
+
+}
+}
+}
+
+#endif
reconstruct solutions for single invocation conjectures in original grammar
option cegqiSingleInvReconstructConst --cegqi-si-reconstruct-const bool :default true
include constants when reconstruct solutions for single invocation conjectures in original grammar
+option cegqiSingleInvPreRegInst --cegqi-si-prereg-inst bool :default true
+ preregister ground instantiations when single invocation
option cegqiSingleInvAbort --cegqi-si-abort bool :default false
- abort if our synthesis conjecture is not single invocation
+ abort if synthesis conjecture is not single invocation
+option cegqiSingleInvMultiInstAbort --cegqi-si-multi-inst-abort bool :default false
+ abort if synthesis conjecture is single invocation with no ITE in grammar and multiple instantiations are tried
option sygusNormalForm --sygus-nf bool :default true
only search for sygus builtin terms that are in normal form
option quantAlphaEquiv --quant-alpha-equiv bool :default true
infer alpha equivalence between quantified formulas
+
+### recursive function options
+
+#option funDefs --fun-defs bool :default false
+# enable specialized techniques for recursive function definitions
endmodule
Node QuantifiersRewriter::mkForAll( std::vector< Node >& args, Node body, Node ipl ){
std::vector< Node > activeArgs;
- computeArgVec2( args, activeArgs, body, ipl );
+ //if cegqi is on, may be synthesis conjecture, in which case we want to keep all variables
+ if( options::ceGuidedInst() && !ipl.isNull() ){
+ for( unsigned i=0; i<ipl.getNumChildren(); i++ ){
+ Trace("quant-attr-debug") << "Check : " << ipl[i] << " " << ipl[i].getKind() << std::endl;
+ if( ipl[i].getKind()==INST_ATTRIBUTE ){
+ Node avar = ipl[i][0];
+ if( avar.getAttribute(SygusAttribute()) ){
+ activeArgs.insert( activeArgs.end(), args.begin(), args.end() );
+ }
+ }
+ }
+ }
+ if( activeArgs.empty() ){
+ computeArgVec2( args, activeArgs, body, ipl );
+ }
if( activeArgs.empty() ){
return body;
}else{
#include "theory/datatypes/datatypes_rewriter.h"
#include "theory/quantifiers/ce_guided_instantiation.h"
#include "theory/quantifiers/rewrite_engine.h"
+#include "theory/quantifiers/fun_def_engine.h"
//for sygus
#include "theory/bv/theory_bv_utils.h"
exit( 0 );
}
d_fun_defs[f] = true;
+ d_quantEngine->setOwner( q, d_quantEngine->getFunDefEngine() );
}
if( avar.getAttribute(SygusAttribute()) ){
//not necessarily nested existential
}
}
-TypeNode TermDbSygus::getSygusType( Node v ) {
+TypeNode TermDbSygus::getSygusTypeForVar( Node v ) {
Assert( d_fv_stype.find( v )!=d_fv_stype.end() );
return d_fv_stype[v];
}
Node n = NodeManager::currentNM()->mkNode( APPLY, children );
//must expand definitions
Node ne = Node::fromExpr( smt::currentSmtEngine()->expandDefinitions( n.toExpr() ) );
- Trace("sygus-util-debug") << "Expanded definitions in " << n << " to " << ne << std::endl;
+ Trace("sygus-db-debug") << "Expanded definitions in " << n << " to " << ne << std::endl;
return ne;
*/
}
d_register[tn] = TypeNode::null();
}else{
const Datatype& dt = ((DatatypeType)(tn).toType()).getDatatype();
- Trace("sygus-util") << "Register type " << dt.getName() << "..." << std::endl;
+ Trace("sygus-db") << "Register type " << dt.getName() << "..." << std::endl;
d_register[tn] = TypeNode::fromType( dt.getSygusType() );
if( d_register[tn].isNull() ){
- Trace("sygus-util") << "...not sygus." << std::endl;
+ Trace("sygus-db") << "...not sygus." << std::endl;
}else{
//for constant reconstruction
Kind ck = getComparisonKind( TypeNode::fromType( dt.getSygusType() ) );
Expr sop = dt[i].getSygusOp();
Assert( !sop.isNull() );
Node n = Node::fromExpr( sop );
- Trace("sygus-util") << " Operator #" << i << " : " << sop;
+ Trace("sygus-db") << " Operator #" << i << " : " << sop;
if( sop.getKind() == kind::BUILTIN ){
Kind sk = NodeManager::operatorToKind( n );
- Trace("sygus-util") << ", kind = " << sk;
+ Trace("sygus-db") << ", kind = " << sk;
d_kinds[tn][sk] = i;
d_arg_kind[tn][i] = sk;
}else if( sop.isConst() ){
- Trace("sygus-util") << ", constant";
+ Trace("sygus-db") << ", constant";
d_consts[tn][n] = i;
d_arg_const[tn][i] = n;
d_const_list[tn].push_back( n );
}
d_ops[tn][n] = i;
d_arg_ops[tn][i] = n;
- Trace("sygus-util") << std::endl;
+ Trace("sygus-db") << std::endl;
}
//sort the constant list
if( !d_const_list[tn].empty() ){
sc.d_tds = this;
std::sort( d_const_list[tn].begin(), d_const_list[tn].end(), sc );
}
- Trace("sygus-util") << "Type has " << d_const_list[tn].size() << " constants..." << std::endl << " ";
+ Trace("sygus-db") << "Type has " << d_const_list[tn].size() << " constants..." << std::endl << " ";
for( unsigned i=0; i<d_const_list[tn].size(); i++ ){
- Trace("sygus-util") << d_const_list[tn][i] << " ";
+ Trace("sygus-db") << d_const_list[tn][i] << " ";
}
- Trace("sygus-util") << std::endl;
- Trace("sygus-util") << "Of these, " << d_const_list_pos[tn] << " are marked as positive." << std::endl;
+ Trace("sygus-db") << std::endl;
+ Trace("sygus-db") << "Of these, " << d_const_list_pos[tn] << " are marked as positive." << std::endl;
}
//register connected types
for( unsigned i=0; i<dt.getNumConstructors(); i++ ){
return d_register.find( tn )!=d_register.end();
}
+TypeNode TermDbSygus::sygusToBuiltinType( TypeNode tn ) {
+ Assert( isRegistered( tn ) );
+ return d_register[tn];
+}
+
int TermDbSygus::getKindArg( TypeNode tn, Kind k ) {
Assert( isRegistered( tn ) );
std::map< TypeNode, std::map< Kind, int > >::iterator itt = d_kinds.find( tn );
return com==d_true;
}
+
void doStrReplace(std::string& str, const std::string& oldStr, const std::string& newStr){
size_t pos = 0;
while((pos = str.find(oldStr, pos)) != std::string::npos){
if( n.getNumChildren()>0 ){
out << "(";
}
- out << dt[cIndex].getSygusOp();
+ Node op = dt[cIndex].getSygusOp();
+ if( op.getType().isBitVector() && op.isConst() ){
+ //print in the style it was given
+ Trace("sygus-print-bvc") << "[Print " << op << " " << dt[cIndex].getName() << "]" << std::endl;
+ std::stringstream ss;
+ ss << dt[cIndex].getName();
+ std::string str = ss.str();
+ std::size_t found = str.find_last_of("_");
+ Assert( found!=std::string::npos );
+ std::string name = std::string( str.begin() + found +1, str.end() );
+ out << name;
+ }else{
+ out << op;
+ }
if( n.getNumChildren()>0 ){
for( unsigned i=0; i<n.getNumChildren(); i++ ){
out << " ";
out << ")";
}
}else{
+ std::stringstream let_out;
//print as let term
if( dt[cIndex].getNumSygusLetInputArgs()>0 ){
- out << "(let (";
+ let_out << "(let (";
}
std::vector< Node > subs_lvs;
std::vector< Node > new_lvs;
//map free variables to proper terms
if( i<dt[cIndex].getNumSygusLetInputArgs() ){
//it should be printed as a let argument
- out << "(";
- out << lv << " " << lv.getType() << " ";
- printSygusTerm( out, n[i], lvs );
- out << ")";
+ let_out << "(";
+ let_out << lv << " " << lv.getType() << " ";
+ printSygusTerm( let_out, n[i], lvs );
+ let_out << ")";
}
}
if( dt[cIndex].getNumSygusLetInputArgs()>0 ){
- out << ") ";
+ let_out << ") ";
}
//print the body
Node let_body = Node::fromExpr( dt[cIndex].getSygusLetBody() );
let_body = let_body.substitute( subs_lvs.begin(), subs_lvs.end(), new_lvs.begin(), new_lvs.end() );
new_lvs.insert( new_lvs.end(), lvs.begin(), lvs.end() );
- std::stringstream body_out;
- printSygusTerm( body_out, let_body, new_lvs );
- std::string body = body_out.str();
+ printSygusTerm( let_out, let_body, new_lvs );
+ if( dt[cIndex].getNumSygusLetInputArgs()>0 ){
+ let_out << ")";
+ }
+ //do variable substitutions since ASSUMING : let_vars are interpreted literally and do not represent a class of variables
+ std::string lbody = let_out.str();
for( unsigned i=0; i<dt[cIndex].getNumSygusLetArgs(); i++ ){
std::stringstream old_str;
old_str << new_lvs[i];
}else{
new_str << Node::fromExpr( dt[cIndex].getSygusLetArg( i ) );
}
- doStrReplace( body, old_str.str().c_str(), new_str.str().c_str() );
- }
- out << body;
- if( dt[cIndex].getNumSygusLetInputArgs()>0 ){
- out << ")";
+ doStrReplace( lbody, old_str.str().c_str(), new_str.str().c_str() );
}
+ out << lbody;
}
return;
}
bool getMatch( Node n, TypeNode st, int& index_found, std::vector< Node >& args, int index_exc = -1, int index_start = 0 );
private:
//information for sygus types
- std::map< TypeNode, TypeNode > d_register; //stores sygus type
+ std::map< TypeNode, TypeNode > d_register; //stores sygus -> builtin type
std::map< TypeNode, std::map< int, Kind > > d_arg_kind;
std::map< TypeNode, std::map< Kind, int > > d_kinds;
std::map< TypeNode, std::map< int, Node > > d_arg_const;
public:
TermDbSygus();
bool isRegistered( TypeNode tn );
+ TypeNode sygusToBuiltinType( TypeNode tn );
int getKindArg( TypeNode tn, Kind k );
int getConstArg( TypeNode tn, Node n );
int getOpArg( TypeNode tn, Node n );
Node getTypeValueOffset( TypeNode tn, Node val, int offset, int& status );
/** get value */
Node getTypeMaxValue( TypeNode tn );
- TypeNode getSygusType( Node v );
+ TypeNode getSygusTypeForVar( Node v );
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 );
#include "theory/uf/theory_uf.h"
#include "theory/quantifiers/full_model_check.h"
#include "theory/quantifiers/ambqi_builder.h"
+#include "theory/quantifiers/fun_def_engine.h"
using namespace std;
using namespace CVC4;
}else{
d_alpha_equiv = NULL;
}
+ //if( options::funDefs() ){
+ // d_fun_def_engine = new quantifiers::FunDefEngine( this, c );
+ // d_modules.push_back( d_fun_def_engine );
+ //}else{
+ d_fun_def_engine = NULL;
+ //}
if( needsBuilder ){
Trace("quant-engine-debug") << "Initialize model engine, mbqi : " << options::mbqiMode() << " " << options::fmfBoundInt() << std::endl;
delete d_sg_gen;
delete d_ceg_inst;
delete d_lte_part_inst;
+ delete d_fun_def_engine;
for(std::map< Node, QuantPhaseReq* >::iterator i = d_phase_reqs.begin(); i != d_phase_reqs.end(); ++i) {
delete (*i).second;
}
class CegInstantiation;
class LtePartialInst;
class AlphaEquivalence;
+ class FunDefEngine;
}/* CVC4::theory::quantifiers */
namespace inst {
quantifiers::CegInstantiation * d_ceg_inst;
/** lte partial instantiation */
quantifiers::LtePartialInst * d_lte_part_inst;
+ /** function definitions engine */
+ quantifiers::FunDefEngine * d_fun_def_engine;
public: //effort levels
enum {
QEFFORT_CONFLICT,
quantifiers::CegInstantiation * getCegInstantiation() { return d_ceg_inst; }
/** local theory ext partial inst */
quantifiers::LtePartialInst * getLtePartialInst() { return d_lte_part_inst; }
+ /** function definition engine */
+ quantifiers::FunDefEngine * getFunDefEngine() { return d_fun_def_engine; }
private:
/** owner of quantified formulas */
std::map< Node, QuantifiersModule * > d_owner;
let-simp.sy \
tl-type.sy \
dup-op.sy \
- nflat-fwd.sy
+ nflat-fwd.sy \
+ nflat-fwd-3.sy \
+ enum-test.sy \
+ no-syntax-test-bool.sy \
+ inv-example.sy \
+ uminus_one.sy
# sygus tests currently taking too long for make regress
EXTRA_DIST = $(TESTS) \
--- /dev/null
+; EXPECT: unsat
+; COMMAND-LINE: --cegqi-si
+(set-logic LIA)
+(define-sort D (Enum (a b)))
+(define-fun f ((x D)) Int (ite (= x D::a) 3 7))
+(synth-fun g () D ((Start D (D::a D::b))))
+(constraint (= (f g) 7))
+(check-synth)
\ No newline at end of file
--- /dev/null
+; EXPECT: unsat
+; COMMAND-LINE: --cegqi-si
+(set-logic LIA)
+(synth-inv inv-f ((x Int) (y Int) (b Bool)))
+(declare-primed-var x Int)
+(declare-primed-var y Int)
+(declare-primed-var b Bool)
+(define-fun pre-f ((x Int) (y Int) (b Bool)) Bool (and (and (>= x 5) (<= x 9)) (and (>= y 1) (<= y 3))))
+(define-fun trans-f ((x Int) (y Int) (b Bool) (x! Int) (y! Int) (b! Bool)) Bool (and (and (= b! b) (= y! x)) (ite b (= x! (+ x 10)) (= x! (+ x 12)))))
+(define-fun post-f ((x Int) (y Int) (b Bool)) Bool (<= y x))
+(inv-constraint inv-f pre-f trans-f post-f)
+(check-synth)
\ No newline at end of file
--- /dev/null
+; EXPECT: unsat
+; COMMAND-LINE: --cegqi-si
+(set-logic LIA)
+(synth-fun f ((x Int)) Int
+ ((Start Int ((+ (+ Con Con) Con) x))
+ (Con Int (0 1))))
+
+(declare-var x Int)
+(constraint (= (f x) 2))
+(check-synth)
+
--- /dev/null
+; EXPECT: unsat
+; COMMAND-LINE: --cegqi-si
+
+(set-logic LIA)
+
+(synth-fun f ((x Int) (y Int)) Bool)
+
+(declare-var x Int)
+(declare-var y Int)
+
+(constraint (= (f x y) (>= (+ x y) 500)))
+
+
+(check-synth)
+
--- /dev/null
+; EXPECT: unsat
+; COMMAND-LINE: --cegqi
+(set-logic LIA)
+(synth-fun f ((x Int)) Int ((Start Int ((- 1)))))
+(declare-var x Int)
+(constraint (= (f x) (- 1)))
+(check-synth)
\ No newline at end of file
projects / cvc5.git / commitdiff