}
Expr sop = ops[sub_dt_index][0];
Type curr_t;
- if( sop.getKind() != kind::BUILTIN && ( sop.isConst() || sop.getNumChildren()==0 ) ){
+ if( sop.getKind() != kind::BUILTIN && ( sop.isConst() || cargs[sub_dt_index][0].empty() ) ){
curr_t = sop.getType();
- Debug("parser-sygus") << ": it is constant/0-arg cons " << sop << " with type " << sop.getType() << std::endl;
+ Debug("parser-sygus") << ": it is constant/0-arg cons " << sop << " with type " << sop.getType() << ", debug=" << sop.isConst() << " " << cargs[sub_dt_index][0].size() << std::endl;
sygus_to_builtin_expr[t] = sop;
- d_sygus_bound_var_type[sop] = t;
+ //store that term sop has dedicated sygus type t
+ if( d_sygus_bound_var_type.find( sop )==d_sygus_bound_var_type.end() ){
+ d_sygus_bound_var_type[sop] = t;
+ }
}else{
std::vector< Expr > children;
if( sop.getKind() != kind::BUILTIN ){
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() ){
Type bt = sygus_to_builtin[cargs[sub_dt_index][0][i]];
- Debug("parser-sygus") << ": type elem " << i << " " << cargs[sub_dt_index][0][i] << " " << bt << std::endl;
+ Debug("parser-sygus") << ": child " << i << " introduce type elem for " << cargs[sub_dt_index][0][i] << " " << bt << std::endl;
std::stringstream ss;
ss << t << "_x_" << i;
Expr bv = mkBoundVar(ss.str(), bt);
children.push_back( bv );
d_sygus_bound_var_type[bv] = cargs[sub_dt_index][0][i];
}else{
+ Debug("parser-sygus") << ": child " << i << " existing sygus to builtin expr : " << it->second << std::endl;
children.push_back( it->second );
}
}
cnames[index].pop_back();
cnames[index].push_back(ss.str());
- //TODO : mark function as let constructor
- d_sygus_let_func_to_vars[let_func].insert( d_sygus_let_func_to_vars[let_func].end(), let_vars.begin(), let_vars.end() );
+ //mark function as let constructor
+ d_sygus_let_func_to_vars[let_func].insert( d_sygus_let_func_to_vars[let_func].end(), let_define_args.begin(), let_define_args.end() );
d_sygus_let_func_to_body[let_func] = let_body;
+ d_sygus_let_func_to_num_input_vars[let_func] = let_vars.size();
}
testerId.append(name);
checkDeclaration(name, CHECK_UNDECLARED, SYM_VARIABLE);
checkDeclaration(testerId, CHECK_UNDECLARED, SYM_VARIABLE);
- CVC4::DatatypeConstructor c(name, testerId, ops[i] );
+ CVC4::DatatypeConstructor c(name, testerId );
+ Debug("parser-sygus") << "--> Add constructor " << cnames[i] << " to " << dt.getName() << std::endl;
+ Expr let_body;
+ std::vector< Expr > let_args;
+ unsigned let_num_input_args = 0;
+ std::map< CVC4::Expr, CVC4::Expr >::iterator it = d_sygus_let_func_to_body.find( ops[i] );
+ if( it!=d_sygus_let_func_to_body.end() ){
+ let_body = it->second;
+ let_args.insert( let_args.end(), d_sygus_let_func_to_vars[ops[i]].begin(), d_sygus_let_func_to_vars[ops[i]].end() );
+ let_num_input_args = d_sygus_let_func_to_num_input_vars[ops[i]];
+ Debug("parser-sygus") << " it is a let gterm with body " << let_body << std::endl;
+ }
+ c.setSygus( ops[i], let_body, let_args, let_num_input_args );
for( unsigned j=0; j<cargs[i].size(); j++ ){
std::stringstream sname;
sname << name << "_" << j;
c.addArg(sname.str(), cargs[i][j]);
}
- Debug("parser-sygus") << "--> Add constructor " << cnames[i] << " to " << dt.getName() << std::endl;
dt.addConstructor(c);
}
}
std::map< CVC4::Expr, CVC4::Type > d_sygus_bound_var_type;
std::map< CVC4::Expr, std::vector< CVC4::Expr > > d_sygus_let_func_to_vars;
std::map< CVC4::Expr, CVC4::Expr > d_sygus_let_func_to_body;
+ std::map< CVC4::Expr, unsigned > d_sygus_let_func_to_num_input_vars;
void collectSygusLetArgs( CVC4::Expr e, std::vector< CVC4::Type >& sygusArgs, std::vector< CVC4::Expr >& builtinArgs );
if( options::recurseCbqi() || options::cbqi2() ){
options::cbqi.set( true );
}
+ if( options::cbqi2() ){
+ if( !options::rewriteDivk.wasSetByUser()) {
+ options::rewriteDivk.set( true );
+ }
+ }
if( options::cbqi() ){
if( !options::quantConflictFind.wasSetByUser() ){
options::quantConflictFind.set( false );
Node progc = prog;
if( options::sygusNormalFormGlobalArg() ){
bool argChanged = false;
+ Trace("sygus-nf-gen-debug") << "Check replacements on " << prog << " " << prog.getKind() << std::endl;
for( unsigned i=0; i<prog.getNumChildren(); i++ ){
Node prev = children[i];
children[i] = d_tds->getVarInc( children_stype[i], var_count );
+ if( parentOpKind!=kind::BUILTIN ){
+ children.insert( children.begin(), prog.getOperator() );
+ }
Node progcn = NodeManager::currentNM()->mkNode( prog.getKind(), children );
+ if( parentOpKind!=kind::BUILTIN ){
+ children.erase( children.begin(), children.begin() + 1 );
+ }
Node progcr = Rewriter::rewrite( progcn );
Trace("sygus-nf-gen-debug") << "Var replace argument " << i << " : " << progcn << " -> " << progcr << std::endl;
if( progcr==progr ){
TypeNode tn = nv.getType();
Trace("cegqi-engine") << n[i] << " -> ";
std::stringstream ss;
- printSygusTerm( ss, nv );
+ std::vector< Node > lvs;
+ TermDbSygus::printSygusTerm( ss, nv, lvs );
Trace("cegqi-engine") << ss.str() << " ";
}
if( nv.isNull() ){
if( sol.isNull() ){
out << "?";
}else{
- printSygusTerm( out, sol );
+ std::vector< Node > lvs;
+ TermDbSygus::printSygusTerm( out, sol, lvs );
}
}
out << ")" << std::endl;
}
}
-void CegInstantiation::printSygusTerm( std::ostream& out, Node n ) {
- if( n.getKind()==APPLY_CONSTRUCTOR ){
- TypeNode tn = n.getType();
- const Datatype& dt = ((DatatypeType)(tn).toType()).getDatatype();
- if( dt.isSygus() ){
- int cIndex = Datatype::indexOf( n.getOperator().toExpr() );
- Assert( !dt[cIndex].getSygusOp().isNull() );
- if( n.getNumChildren()>0 ){
- out << "(";
- }
- out << dt[cIndex].getSygusOp();
- if( n.getNumChildren()>0 ){
- for( unsigned i=0; i<n.getNumChildren(); i++ ){
- out << " ";
- printSygusTerm( out, n[i] );
- }
- out << ")";
- }
- return;
- }
- }else if( !n.getAttribute(SygusProxyAttribute()).isNull() ){
- out << n.getAttribute(SygusProxyAttribute());
- }else{
- out << n;
- }
-}
-
void CegInstantiation::collectDisjuncts( Node n, std::vector< Node >& d ) {
if( n.getKind()==OR ){
for( unsigned i=0; i<n.getNumChildren(); i++ ){
Node getModelValue( Node n );
/** get model term */
Node getModelTerm( Node n );
-private:
- /** print sygus term */
- void printSygusTerm( std::ostream& out, Node n );
public:
CegInstantiation( QuantifiersEngine * qe, context::Context* c );
public:
std::map< TypeNode, int > var_count;
std::map< int, Node > pre;
Node g = mkGeneric( dt, c, var_count, pre );
+ Trace("sygus-db-debug") << "Sygus DB : Generic is " << g << std::endl;
Node gr = Rewriter::rewrite( g );
+ Trace("sygus-db-debug") << "Sygus DB : Generic rewritten is " << gr << std::endl;
gr = Node::fromExpr( smt::currentSmtEngine()->expandDefinitions( gr.toExpr() ) );
Trace("sygus-db") << "Sygus DB : Generic base " << dt[c].getName() << " : " << gr << std::endl;
d_generic_base[tn][c] = gr;
if( op.getKind()!=BUILTIN ){
children.push_back( op );
}
+ Trace("sygus-db") << "mkGeneric " << dt.getName() << " " << op << " " << op.getKind() << "..." << std::endl;
for( int i=0; i<(int)dt[c].getNumArgs(); i++ ){
TypeNode tna = TypeNode::fromType( ((SelectorType)dt[c][i].getType()).getRangeType() );
Node a;
Assert( !a.isNull() );
children.push_back( a );
}
+ Node ret;
if( op.getKind()==BUILTIN ){
- return NodeManager::currentNM()->mkNode( op, children );
+ ret = NodeManager::currentNM()->mkNode( op, children );
}else{
if( children.size()==1 ){
- return children[0];
+ ret = children[0];
}else{
- return NodeManager::currentNM()->mkNode( APPLY, children );
+ ret = NodeManager::currentNM()->mkNode( APPLY, children );
/*
Node n = NodeManager::currentNM()->mkNode( APPLY, children );
//must expand definitions
*/
}
}
+ Trace("sygus-db") << "...returning " << ret << std::endl;
+ return ret;
}
Node TermDbSygus::sygusToBuiltin( Node n, TypeNode tn ) {
pre[j] = sygusToBuiltin( n[j], getArgType( dt[i], j ) );
}
Node ret = mkGeneric( dt, i, var_count, pre );
+ Trace("sygus-db-debug") << "SygusToBuiltin : Generic is " << ret << std::endl;
ret = Node::fromExpr( smt::currentSmtEngine()->expandDefinitions( ret.toExpr() ) );
+ Trace("sygus-db-debug") << "SygusToBuiltin : After expand definitions " << ret << std::endl;
d_sygus_to_builtin[tn][n] = ret;
return ret;
}else{
NodeManager::currentNM()->mkNode( AND, t[0].negate(), t[1].negate() ) );
}
return Node::null();
-}
\ No newline at end of file
+}
+
+
+void doReplace(std::string& str, const std::string& oldStr, const std::string& newStr){
+ size_t pos = 0;
+ while((pos = str.find(oldStr, pos)) != std::string::npos){
+ str.replace(pos, oldStr.length(), newStr);
+ pos += newStr.length();
+ }
+}
+
+void TermDbSygus::printSygusTerm( std::ostream& out, Node n, std::vector< Node >& lvs ) {
+ if( n.getKind()==APPLY_CONSTRUCTOR ){
+ TypeNode tn = n.getType();
+ const Datatype& dt = ((DatatypeType)(tn).toType()).getDatatype();
+ if( dt.isSygus() ){
+ int cIndex = Datatype::indexOf( n.getOperator().toExpr() );
+ Assert( !dt[cIndex].getSygusOp().isNull() );
+ if( dt[cIndex].getSygusLetBody().isNull() ){
+ if( n.getNumChildren()>0 ){
+ out << "(";
+ }
+ out << dt[cIndex].getSygusOp();
+ if( n.getNumChildren()>0 ){
+ for( unsigned i=0; i<n.getNumChildren(); i++ ){
+ out << " ";
+ printSygusTerm( out, n[i], lvs );
+ }
+ out << ")";
+ }
+ }else{
+ //print as let term
+ out << "(let (";
+ std::vector< Node > subs_lvs;
+ std::vector< Node > new_lvs;
+ for( unsigned i=0; i<dt[cIndex].getNumSygusLetArgs(); i++ ){
+ Node v = Node::fromExpr( dt[cIndex].getSygusLetArg( i ) );
+ subs_lvs.push_back( v );
+ std::stringstream ss;
+ ss << "_l_" << new_lvs.size();
+ Node lv = NodeManager::currentNM()->mkBoundVar( ss.str(), v.getType() );
+ new_lvs.push_back( lv );
+ //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 << ")";
+ }
+ }
+ 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();
+ for( unsigned i=dt[cIndex].getNumSygusLetInputArgs(); i<dt[cIndex].getNumSygusLetArgs(); i++ ){
+ std::stringstream old_str;
+ old_str << new_lvs[i];
+ std::stringstream new_str;
+ printSygusTerm( new_str, n[i], lvs );
+ doReplace( body, old_str.str().c_str(), new_str.str().c_str() );
+ }
+ out << body << ")";
+ }
+ return;
+ }
+ }else if( !n.getAttribute(SygusProxyAttribute()).isNull() ){
+ out << n.getAttribute(SygusProxyAttribute());
+ }else{
+ out << n;
+ }
+}
+
Node minimizeBuiltinTerm( Node n );
/** given a term, expand it into more basic components */
Node expandBuiltinTerm( Node n );
+ /** print sygus term */
+ static void printSygusTerm( std::ostream& out, Node n, std::vector< Node >& lvs );
};
}/* CVC4::theory::quantifiers namespace */
CheckArgument(!tester.empty(), tester, "cannot construct a datatype constructor without a tester");
}
-DatatypeConstructor::DatatypeConstructor(std::string name, std::string tester, Expr sygus_op) :
- d_name(name + '\0' + tester),
- d_tester(),
- d_args(),
- d_sygus_op(sygus_op) {
- CheckArgument(name != "", name, "cannot construct a datatype constructor without a name");
- CheckArgument(!tester.empty(), tester, "cannot construct a datatype constructor without a tester");
+void DatatypeConstructor::setSygus( Expr op, Expr let_body, std::vector< Expr >& let_args, unsigned num_let_input_args ){
+ d_sygus_op = op;
+ d_sygus_let_body = let_body;
+ d_sygus_let_args.insert( d_sygus_let_args.end(), let_args.begin(), let_args.end() );
+ d_sygus_num_let_input_args = num_let_input_args;
}
+
void DatatypeConstructor::addArg(std::string selectorName, Type selectorType) {
// We don't want to introduce a new data member, because eventually
// we're going to be a constant stuffed inside a node. So we stow
return d_sygus_op;
}
+Expr DatatypeConstructor::getSygusLetBody() const {
+ CheckArgument(isResolved(), this, "this datatype constructor is not yet resolved");
+ return d_sygus_let_body;
+}
+
+unsigned DatatypeConstructor::getNumSygusLetArgs() const {
+ CheckArgument(isResolved(), this, "this datatype constructor is not yet resolved");
+ return d_sygus_let_args.size();
+}
+
+Expr DatatypeConstructor::getSygusLetArg( unsigned i ) const {
+ CheckArgument(isResolved(), this, "this datatype constructor is not yet resolved");
+ return d_sygus_let_args[i];
+}
+
+unsigned DatatypeConstructor::getNumSygusLetInputArgs() const {
+ CheckArgument(isResolved(), this, "this datatype constructor is not yet resolved");
+ return d_sygus_num_let_input_args;
+}
+
Cardinality DatatypeConstructor::getCardinality() const throw(IllegalArgumentException) {
CheckArgument(isResolved(), this, "this datatype constructor is not yet resolved");
std::vector<DatatypeConstructorArg> d_args;
/** the operator associated with this constructor (for sygus) */
Expr d_sygus_op;
+ Expr d_sygus_let_body;
+ std::vector< Expr > d_sygus_let_args;
+ unsigned d_sygus_num_let_input_args;
void resolve(ExprManager* em, DatatypeType self,
const std::map<std::string, DatatypeType>& resolutions,
* constructor and tester aren't created until resolution time.
*/
DatatypeConstructor(std::string name, std::string tester);
- DatatypeConstructor(std::string name, std::string tester, Expr sygus_op);
+
+ /** set sygus */
+ void setSygus( Expr op, Expr let_body, std::vector< Expr >& let_args, unsigned num_let_input_argus );
/**
* Add an argument (i.e., a data field) of the given name and type
/** get sygus op */
Expr getSygusOp() const;
-
+ /** get sygus let body */
+ Expr getSygusLetBody() const;
+ /** get number of sygus let args */
+ unsigned getNumSygusLetArgs() const;
+ /** get sygus let arg */
+ Expr getSygusLetArg( unsigned i ) const;
+ /** get number of let arguments that should be printed as arguments to let */
+ unsigned getNumSygusLetInputArgs() const;
+
/**
* Get the tester name for this Datatype constructor.
*/
const-var-test.sy \
no-syntax-test.sy \
no-syntax-test-no-si.sy \
- no-flat-simp.sy
+ no-flat-simp.sy \
+ twolets2-orig.sy \
+ let-ringer.sy \
+ let-simp.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-fun g ((x Int)) Int (ite (= x 1) 15 19))
+(synth-fun f ((x Int)) Int
+ ((Start Int (x
+ 0
+ 1
+ (- Start Start)
+ (let ((z Int Start) (w Int Start)) (+ z (+ x (+ x (+ Start (+ 1 (+ (g w) z)))))))))))
+
+(declare-var x Int)
+(constraint (= (f x) (+ (* 4 x) 15)))
+(check-synth)
--- /dev/null
+; EXPECT: unsat
+; COMMAND-LINE: --cegqi-si
+(set-logic LIA)
+(synth-fun f ((x Int) (y Int)) Int
+ ((Start Int (x
+ y
+ 0
+ (- Start Start)
+ (let ((z Int Start)) (+ z z))))))
+
+(declare-var x Int)
+(declare-var y Int)
+(constraint (= (f x y) (* 3 x)))
+(check-synth)
+
--- /dev/null
+; EXPECT: unsat
+; COMMAND-LINE: --cegqi-si
+(set-logic LIA)
+(synth-fun f1 ((x Int)) Int
+ (
+ (Start Int (
+ (let ((y Int CInt) (z Int CInt)) (+ (+ y x) z))
+ )
+ )
+ (CInt Int (0 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15))
+
+ )
+)
+(synth-fun f2 ((x Int)) Int
+ (
+ (Start Int (x
+ (let ((y Int Start) (z Int CInt)) (+ (+ y x) z))
+ )
+ )
+ (CInt Int (0 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15))
+
+ )
+)
+(declare-var x1 Int)
+(declare-var x2 Int)
+(constraint (= (+ (f1 x1)(f2 x2)) (+ (+ x2 x2) (+ x1 8))))
+(check-synth)
+
projects / cvc5.git / commitdiff