printer/dagification_visitor.h \
printer/printer.cpp \
printer/printer.h \
+ printer/sygus_print_callback.cpp \
+ printer/sygus_print_callback.h \
printer/ast/ast_printer.cpp \
printer/ast/ast_printer.h \
printer/cvc/cvc_printer.cpp \
d_sygus_allow_all = allow_all;
}
-void Datatype::addSygusConstructor( 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 ) {
+void Datatype::addSygusConstructor(CVC4::Expr op,
+ std::string& cname,
+ std::vector<CVC4::Type>& cargs,
+ std::shared_ptr<SygusPrintCallback> spc)
+{
Debug("dt-sygus") << "--> Add constructor " << cname << " to " << getName() << std::endl;
- if( !let_body.isNull() ){
- Debug("dt-sygus") << " let body = " << let_body << ", args = " << let_args.size() << "," << let_num_input_args << std::endl;
- //TODO : remove arguments not occurring in body
- //if this is a self identity function, ignore
- if( let_args.size()==0 && let_args[0]==let_body ){
- Debug("dt-sygus") << " identity function " << cargs[0] << " to " << getName() << std::endl;
- //TODO
- }
- }
+ Debug("dt-sygus") << " sygus op : " << op << std::endl;
std::string name = getName() + "_" + cname;
std::string testerId("is-");
testerId.append(name);
- //checkDeclaration(name, CHECK_UNDECLARED, SYM_VARIABLE);
- //checkDeclaration(testerId, CHECK_UNDECLARED, SYM_VARIABLE);
CVC4::DatatypeConstructor c(name, testerId );
- c.setSygus( op, let_body, let_args, let_num_input_args );
+ c.setSygus(op, spc);
for( unsigned j=0; j<cargs.size(); j++ ){
Debug("parser-sygus-debug") << " arg " << j << " : " << cargs[j] << std::endl;
std::stringstream sname;
}
addConstructor(c);
}
-
-void Datatype::addSygusConstructor( 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 = 0;
- addSygusConstructor( op, cname, cargs, let_body, let_args, let_num_input_args );
-}
void Datatype::setTuple() {
PrettyCheckArgument(!d_resolved, this, "cannot set tuple to a finalized Datatype");
d_name(name + '\0' + "is_" + name), // default tester name is "is_FOO"
d_tester(),
d_args(),
- d_sygus_num_let_input_args(0) {
+ d_sygus_pc(nullptr)
+{
PrettyCheckArgument(name != "", name, "cannot construct a datatype constructor without a name");
}
d_name(name + '\0' + tester),
d_tester(),
d_args(),
- d_sygus_num_let_input_args(0) {
+ d_sygus_pc(nullptr)
+{
PrettyCheckArgument(name != "", name, "cannot construct a datatype constructor without a name");
PrettyCheckArgument(!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 ){
+void DatatypeConstructor::setSygus(Expr op,
+ std::shared_ptr<SygusPrintCallback> spc)
+{
+ PrettyCheckArgument(
+ !isResolved(), this, "cannot modify a finalized Datatype constructor");
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;
+ d_sygus_pc = spc;
}
void DatatypeConstructor::addArg(std::string selectorName, Type selectorType) {
return d_sygus_op;
}
-Expr DatatypeConstructor::getSygusLetBody() const {
- PrettyCheckArgument(isResolved(), this, "this datatype constructor is not yet resolved");
- return d_sygus_let_body;
-}
-
-unsigned DatatypeConstructor::getNumSygusLetArgs() const {
- PrettyCheckArgument(isResolved(), this, "this datatype constructor is not yet resolved");
- return d_sygus_let_args.size();
-}
-
-Expr DatatypeConstructor::getSygusLetArg( unsigned i ) const {
- PrettyCheckArgument(isResolved(), this, "this datatype constructor is not yet resolved");
- return d_sygus_let_args[i];
-}
-
-unsigned DatatypeConstructor::getNumSygusLetInputArgs() const {
- PrettyCheckArgument(isResolved(), this, "this datatype constructor is not yet resolved");
- return d_sygus_num_let_input_args;
-}
-
bool DatatypeConstructor::isSygusIdFunc() const {
PrettyCheckArgument(isResolved(), this, "this datatype constructor is not yet resolved");
- return d_sygus_let_args.size()==1 && d_sygus_let_args[0]==d_sygus_let_body;
+ return (d_sygus_op.getKind() == kind::LAMBDA
+ && d_sygus_op[0].getNumChildren() == 1
+ && d_sygus_op[0][0] == d_sygus_op[1]);
}
SygusPrintCallback* DatatypeConstructor::getSygusPrintCallback() const
{
PrettyCheckArgument(
isResolved(), this, "this datatype constructor is not yet resolved");
- // TODO (#1344) return the stored callback
- return nullptr;
+ return d_sygus_pc.get();
}
Cardinality DatatypeConstructor::getCardinality( Type t ) const throw(IllegalArgumentException) {
{
public:
SygusPrintCallback() {}
- ~SygusPrintCallback() {}
+ virtual ~SygusPrintCallback() {}
/**
* Writes the term that sygus datatype expression e
* encodes to stream out. p is the printer that
*/
DatatypeConstructor(std::string name, std::string tester);
+ ~DatatypeConstructor() {}
/**
* Add an argument (i.e., a data field) of the given name and type
* to this Datatype constructor. Selector names need not be unique;
* deep embedding.
*/
Expr getSygusOp() const;
- /** get sygus let body
- *
- * The sygus official format
- * (http://www.sygus.org/SyGuS-COMP2015.html)
- * allows for let expressions to occur in grammars.
- *
- * TODO (#1344) refactor this
- */
- Expr getSygusLetBody() const;
- /** get number of sygus let args
- * TODO (#1344) refactor this
- */
- unsigned getNumSygusLetArgs() const;
- /** get sygus let arg
- * TODO (#1344) refactor this
- */
- Expr getSygusLetArg( unsigned i ) const;
- /** get number of let arguments that should be printed as arguments to let
- * TODO (#1344) refactor this
- */
- unsigned getNumSygusLetInputArgs() const;
/** is this a sygus identity function?
- * TODO (#1344) refactor this
+ *
+ * This returns true if the sygus operator of this datatype constructor is
+ * of the form (lambda (x) x).
*/
bool isSygusIdFunc() const;
/** get sygus print callback
int getSelectorIndexInternal( Expr sel ) const;
/** involves external type
+ *
* Get whether this constructor has a subfield
* in any constructor that is not a datatype type.
*/
bool involvesExternalType() const;
/** involves external type
+ *
* Get whether this constructor has a subfield
* in any constructor that is an uninterpreted type.
*/
/** set sygus
*
- * Set that this constructor is a sygus datatype
- * constructor that encodes operator op.
- * The remaining arguments are for handling
- * let expressions in user-provided sygus
- * grammars (see above).
+ * Set that this constructor is a sygus datatype constructor that encodes
+ * operator op. spc is the sygus callback of this datatype constructor,
+ * which is stored in a shared pointer.
*/
- void setSygus( Expr op, Expr let_body, std::vector< Expr >& let_args, unsigned num_let_input_argus );
+ void setSygus(Expr op, std::shared_ptr<SygusPrintCallback> spc);
private:
/** the name of the constructor */
std::vector<DatatypeConstructorArg> d_args;
/** sygus operator */
Expr d_sygus_op;
- /** sygus let body */
- Expr d_sygus_let_body;
- /** sygus let args */
- std::vector<Expr> d_sygus_let_args;
- /** sygus num let input args */
- unsigned d_sygus_num_let_input_args;
+ /** sygus print callback */
+ std::shared_ptr<SygusPrintCallback> d_sygus_pc;
/** shared selectors for each type
+ *
* This stores the shared (constructor-agnotic)
* selectors that access the fields of this datatype.
* In the terminology of "Datatypes with Shared Selectors",
* this constructor encodes
* cname : the name of the constructor (for printing only)
* cargs : the arguments of the constructor
+ * spc : an (optional) callback that is used for custom printing. This is
+ * to accomodate user-provided grammars in the sygus format.
*
* It should be the case that cargs are sygus datatypes that
* encode the arguments of op. For example, a sygus constructor
* with op = PLUS should be such that cargs.size()>=2 and
* the sygus type of cargs[i] is Real/Int for each i.
*/
- void addSygusConstructor( CVC4::Expr op, std::string& cname, std::vector< CVC4::Type >& cargs );
- /** add sygus constructor (for let expression constructors)
- *
- * This adds a sygus constructor to this datatype, where
- * this datatype should be currently unresolved.
- *
- * In contrast to the above function, the constructor we
- * add corresponds to a let expression if let_body is
- * non-null. For details, see documentation for
- * DatatypeConstructor::getSygusLetBody above.
- */
- void addSygusConstructor( 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 );
+ void addSygusConstructor(CVC4::Expr op,
+ std::string& cname,
+ std::vector<CVC4::Type>& cargs,
+ std::shared_ptr<SygusPrintCallback> spc = nullptr);
/** set that this datatype is a tuple */
void setTuple();
option dumpInstantiations --dump-instantiations bool :default false
output instantiations of quantified formulas after every UNSAT/VALID response
option sygusOut --sygus-out=MODE SygusSolutionOutMode :default SYGUS_SOL_OUT_STATUS_AND_DEF :include "options/sygus_out_mode.h" :handler stringToSygusSolutionOutMode :read-write
- output mode for sygus
+ output mode for sygus
+option sygusPrintCallbacks --sygus-print-callbacks bool :default true
+ use sygus print callbacks to print sygus terms in the user-provided form (disable for debugging)
option dumpSynth --dump-synth bool :read-write :default false
output solution for synthesis conjectures after every UNSAT/VALID response
option unsatCores produce-unsat-cores --produce-unsat-cores bool :predicate proofEnabledBuild :notify :notify notifyBeforeSearch
#include "parser/parser.h"
#include "parser/smt1/smt1.h"
#include "parser/smt2/smt2_input.h"
+#include "printer/sygus_print_callback.h"
#include "smt/command.h"
#include "util/bitvector.h"
std::map< CVC4::Type, CVC4::Type >& sygus_to_builtin ) {
Debug("parser-sygus") << "Making sygus datatype " << dt.getName() << std::endl;
Debug("parser-sygus") << " add constructors..." << std::endl;
- std::vector<std::string> df_name;
- std::vector<CVC4::Expr> df_op;
- std::vector< std::vector<Expr> > df_let_args;
- std::vector< Expr > df_let_body;
- //dt.mkSygusConstructors( ops, cnames, cargs, sygus_to_builtin,
- // d_sygus_let_func_to_vars, d_sygus_let_func_to_body, d_sygus_let_func_to_num_input_vars,
- // df_name, df_op, df_let_args, df_let_body );
Debug("parser-sygus") << "SMT2 sygus parser : Making constructors for sygus datatype " << dt.getName() << std::endl;
Debug("parser-sygus") << " add constructors..." << std::endl;
- for( int i=0; i<(int)cnames.size(); i++ ){
+ for (unsigned i = 0, size = cnames.size(); i < size; i++)
+ {
bool is_dup = false;
bool is_dup_op = false;
- Expr let_body;
- std::vector< Expr > let_args;
- unsigned let_num_input_args = 0;
- for( int j=0; j<i; j++ ){
+ for (unsigned j = 0; j < i; j++)
+ {
if( ops[i]==ops[j] ){
is_dup_op = true;
if( cargs[i].size()==cargs[j].size() ){
}
}
}
+ Debug("parser-sygus") << "SYGUS CONS " << i << " : ";
if( is_dup ){
- Debug("parser-sygus") << "--> Duplicate gterm : " << ops[i] << " at " << i << std::endl;
+ Debug("parser-sygus") << "--> Duplicate gterm : " << ops[i] << std::endl;
ops.erase( ops.begin() + i, ops.begin() + i + 1 );
cnames.erase( cnames.begin() + i, cnames.begin() + i + 1 );
cargs.erase( cargs.begin() + i, cargs.begin() + i + 1 );
i--;
- }else if( is_dup_op ){
- Debug("parser-sygus") << "--> Duplicate gterm operator : " << ops[i] << " at " << i << std::endl;
- //make into define-fun
- std::vector<CVC4::Type> fsorts;
- for( unsigned j=0; j<cargs[i].size(); j++ ){
- Type bt = sygus_to_builtin[cargs[i][j]];
- std::stringstream ss;
- ss << dt.getName() << "_x_" << i << "_" << j;
- Expr v = mkBoundVar(ss.str(), bt);
- let_args.push_back( v );
- fsorts.push_back( bt );
- Debug("parser-sygus") << ": var " << i << " " << v << " with type " << bt << " from " << cargs[i][j] << std::endl;
+ }
+ else
+ {
+ std::shared_ptr<SygusPrintCallback> spc;
+ if (is_dup_op)
+ {
+ Debug("parser-sygus") << "--> Duplicate gterm operator : " << ops[i]
+ << std::endl;
+ // make into define-fun
+ std::vector<Type> ltypes;
+ for (unsigned j = 0, size = cargs[i].size(); j < size; j++)
+ {
+ ltypes.push_back(sygus_to_builtin[cargs[i][j]]);
+ }
+ std::vector<Expr> largs;
+ Expr lbvl = makeSygusBoundVarList(dt, i, ltypes, largs);
+
+ // make the let_body
+ std::vector<Expr> children;
+ if (ops[i].getKind() != kind::BUILTIN)
+ {
+ children.push_back(ops[i]);
+ }
+ children.insert(children.end(), largs.begin(), largs.end());
+ Kind sk = ops[i].getKind() != kind::BUILTIN
+ ? kind::APPLY
+ : getExprManager()->operatorToKind(ops[i]);
+ Expr body = getExprManager()->mkExpr(sk, children);
+ // replace by lambda
+ ops[i] = getExprManager()->mkExpr(kind::LAMBDA, lbvl, body);
+ Debug("parser-sygus") << " ...replace op : " << ops[i] << std::endl;
+ // callback prints as the expression
+ spc = std::make_shared<printer::SygusExprPrintCallback>(body, largs);
}
- //make the let_body
- std::vector< Expr > children;
- if( ops[i].getKind() != kind::BUILTIN ){
- children.push_back( ops[i] );
+ else
+ {
+ std::map<Expr, Expr>::iterator it =
+ d_sygus_let_func_to_body.find(ops[i]);
+ if (it != d_sygus_let_func_to_body.end())
+ {
+ Debug("parser-sygus") << "--> Let expression " << ops[i] << std::endl;
+ Expr let_body = it->second;
+ std::vector<Expr> let_args = d_sygus_let_func_to_vars[ops[i]];
+ unsigned let_num_input_args =
+ d_sygus_let_func_to_num_input_vars[ops[i]];
+ // the operator is just the body for the arguments
+ std::vector<Type> ltypes;
+ for (unsigned j = 0, size = let_args.size(); j < size; j++)
+ {
+ ltypes.push_back(let_args[j].getType());
+ }
+ std::vector<Expr> largs;
+ Expr lbvl = makeSygusBoundVarList(dt, i, ltypes, largs);
+ Expr sbody = let_body.substitute(let_args, largs);
+ ops[i] = getExprManager()->mkExpr(kind::LAMBDA, lbvl, sbody);
+ Debug("parser-sygus") << " ...replace op : " << ops[i] << std::endl;
+ // callback prints as a let expression
+ spc = std::make_shared<printer::SygusLetExprPrintCallback>(
+ let_body, let_args, let_num_input_args);
+ }
+ else if (ops[i].getType().isBitVector() && ops[i].isConst())
+ {
+ Debug("parser-sygus") << "--> Bit-vector constant " << ops[i] << " ("
+ << cnames[i] << ")" << std::endl;
+ // Since there are multiple output formats for bit-vectors and
+ // we are required by sygus standards to print in the exact input
+ // format given by the user, we use a print callback to custom print
+ // the given name.
+ spc = std::make_shared<printer::SygusNamedPrintCallback>(cnames[i]);
+ }
+ else if (isDefinedFunction(ops[i]))
+ {
+ Debug("parser-sygus") << "--> Defined function " << ops[i]
+ << std::endl;
+ // turn f into (lammbda (x) (f x))
+ // in a degenerate case, ops[i] may be a defined constant,
+ // in which case we do not replace by a lambda.
+ if (ops[i].getType().isFunction())
+ {
+ std::vector<Type> ftypes =
+ static_cast<FunctionType>(ops[i].getType()).getArgTypes();
+ std::vector<Expr> largs;
+ Expr lbvl = makeSygusBoundVarList(dt, i, ftypes, largs);
+ largs.insert(largs.begin(), ops[i]);
+ Expr body = getExprManager()->mkExpr(kind::APPLY, largs);
+ ops[i] = getExprManager()->mkExpr(kind::LAMBDA, lbvl, body);
+ Debug("parser-sygus") << " ...replace op : " << ops[i]
+ << std::endl;
+ }
+ else
+ {
+ ops[i] = getExprManager()->mkExpr(kind::APPLY, ops[i]);
+ Debug("parser-sygus") << " ...replace op : " << ops[i]
+ << std::endl;
+ }
+ // keep a callback to say it should be printed with the defined name
+ spc = std::make_shared<printer::SygusNamedPrintCallback>(cnames[i]);
+ }
+ else
+ {
+ Debug("parser-sygus") << "--> Default case " << ops[i] << std::endl;
+ }
}
- children.insert( children.end(), let_args.begin(), let_args.end() );
- Kind sk = ops[i].getKind() != kind::BUILTIN ? kind::APPLY : getExprManager()->operatorToKind(ops[i]);
- Debug("parser-sygus") << ": replace " << ops[i] << " " << ops[i].getKind() << " " << sk << std::endl;
- let_body = getExprManager()->mkExpr( sk, children );
- Debug("parser-sygus") << ": new body of function is " << let_body << std::endl;
-
- Type ft = getExprManager()->mkFunctionType(fsorts, let_body.getType());
- Debug("parser-sygus") << ": function type is " << ft << std::endl;
+ // must rename to avoid duplication
std::stringstream ss;
- ss << dt.getName() << "_df_" << i;
- //replace operator and name
- ops[i] = mkFunction(ss.str(), ft, ExprManager::VAR_FLAG_DEFINED);
+ ss << dt.getName() << "_" << i << "_" << cnames[i];
cnames[i] = ss.str();
- // indicate we need a define function
- df_name.push_back( ss.str() );
- df_op.push_back( ops[i] );
- df_let_args.push_back( let_args );
- df_let_body.push_back( let_body );
-
- //d_sygus_defined_funs.push_back( ops[i] );
- //preemptCommand( new DefineFunctionCommand(ss.str(), ops[i], let_args, let_body) );
- dt.addSygusConstructor( ops[i], cnames[i], cargs[i], let_body, let_args, 0 );
- }else{
- 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]];
- }
- dt.addSygusConstructor( ops[i], cnames[i], cargs[i], let_body, let_args, let_num_input_args );
+ // add the sygus constructor
+ dt.addSygusConstructor(ops[i], cnames[i], cargs[i], spc);
}
}
//identity element
Type bt = dt.getSygusType();
Debug("parser-sygus") << ": make identity function for " << bt << ", argument type " << t << std::endl;
+
std::stringstream ss;
- ss << t << "_x_id";
- Expr let_body = mkBoundVar(ss.str(), bt);
- std::vector< Expr > let_args;
- let_args.push_back( let_body );
- //make the identity function
- Type ft = getExprManager()->mkFunctionType(bt, bt);
- std::stringstream ssid;
- ssid << unresolved_gterm_sym[i] << "_id";
- Expr id_op = mkFunction(ss.str(), ft, ExprManager::VAR_FLAG_DEFINED);
- // indicate we need a define function
- df_name.push_back( ssid.str() );
- df_op.push_back( id_op );
- df_let_args.push_back( let_args );
- df_let_body.push_back( let_body );
-
- //d_sygus_defined_funs.push_back( id_op );
- //preemptCommand( new DefineFunctionCommand(ssid.str(), id_op, let_args, let_body) );
+ ss << t << "_x";
+ Expr var = mkBoundVar(ss.str(), bt);
+ std::vector<Expr> lchildren;
+ lchildren.push_back(
+ getExprManager()->mkExpr(kind::BOUND_VAR_LIST, var));
+ lchildren.push_back(var);
+ Expr id_op = getExprManager()->mkExpr(kind::LAMBDA, lchildren);
+
+ // empty sygus callback (should not be printed)
+ std::shared_ptr<SygusPrintCallback> sepc =
+ std::make_shared<printer::SygusEmptyPrintCallback>();
+
//make the sygus argument list
std::vector< Type > id_carg;
id_carg.push_back( t );
- dt.addSygusConstructor( id_op, unresolved_gterm_sym[i], id_carg, let_body, let_args, 0 );
+ dt.addSygusConstructor(id_op, unresolved_gterm_sym[i], id_carg, sepc);
+
//add to operators
ops.push_back( id_op );
}
}
}
}
-
-
- for( unsigned i=0; i<df_name.size(); i++ ){
- d_sygus_defined_funs.push_back( df_op[i] );
- preemptCommand( new DefineFunctionCommand(df_name[i], df_op[i], df_let_args[i], df_let_body[i]) );
+}
+
+Expr Smt2::makeSygusBoundVarList(Datatype& dt,
+ unsigned i,
+ const std::vector<Type>& ltypes,
+ std::vector<Expr>& lvars)
+{
+ for (unsigned j = 0, size = ltypes.size(); j < size; j++)
+ {
+ std::stringstream ss;
+ ss << dt.getName() << "_x_" << i << "_" << j;
+ Expr v = mkBoundVar(ss.str(), ltypes[j]);
+ lvars.push_back(v);
}
+ return getExprManager()->mkExpr(kind::BOUND_VAR_LIST, lvars);
}
const void Smt2::getSygusPrimedVars( std::vector<Expr>& vars, bool isPrimed ) {
std::map< CVC4::Type, CVC4::Type >& sygus_to_builtin,
std::map< CVC4::Type, CVC4::Expr >& sygus_to_builtin_expr );
+ /** make sygus bound var list
+ *
+ * This is used for converting non-builtin sygus operators to lambda
+ * expressions. It takes as input a datatype and constructor index (for
+ * naming) and a vector of type ltypes.
+ * It appends a bound variable to lvars for each type in ltypes, and returns
+ * a bound variable list whose children are lvars.
+ */
+ Expr makeSygusBoundVarList(Datatype& dt,
+ unsigned i,
+ const std::vector<Type>& ltypes,
+ std::vector<Expr>& lvars);
+
void addArithmeticOperators();
void addBitvectorOperators();
int cIndex = Datatype::indexOf(n.getOperator().toExpr());
Assert(!dt[cIndex].getSygusOp().isNull());
SygusPrintCallback* spc = dt[cIndex].getSygusPrintCallback();
- if (spc != nullptr)
+ if (spc != nullptr && options::sygusPrintCallbacks())
{
spc->toStreamSygus(this, out, n.toExpr());
}
}
else
{
- // cannot convert term to analog, print original
- toStream(out, n, -1, false, 1);
+ Node p = n.getAttribute(theory::SygusPrintProxyAttribute());
+ if (!p.isNull())
+ {
+ out << p;
+ }
+ else
+ {
+ // cannot convert term to analog, print original
+ out << n;
+ }
}
}
#include "printer/sygus_print_callback.h"
+#include "expr/node.h"
+#include "printer/printer.h"
+
using namespace CVC4::kind;
using namespace std;
namespace CVC4 {
namespace printer {
-SygusLetExpressionPrinter::SygusLetExpressionPrinter(
- Node let_body, std::vector<Node>& let_args, unsigned ninput_args)
+SygusExprPrintCallback::SygusExprPrintCallback(Expr body,
+ std::vector<Expr>& args)
+ : d_body(body), d_body_argument(-1)
{
+ d_args.insert(d_args.end(), args.begin(), args.end());
+ for (unsigned i = 0, size = d_args.size(); i < size; i++)
+ {
+ if (d_args[i] == d_body)
+ {
+ d_body_argument = static_cast<int>(i);
+ }
+ }
}
-void SygusLetExpressionConstructorPrinter::doStrReplace(
- std::string& str, const std::string& oldStr, const std::string& newStr)
+void SygusExprPrintCallback::doStrReplace(std::string& str,
+ const std::string& oldStr,
+ const std::string& newStr) const
{
size_t pos = 0;
while ((pos = str.find(oldStr, pos)) != std::string::npos)
}
}
-void SygusLetExpressionConstructorPrinter::toStreamSygus(Printer* p,
- std::ostream& out,
- Expr e)
+void SygusExprPrintCallback::toStreamSygus(const Printer* p,
+ std::ostream& out,
+ Expr e) const
+{
+ // optimization: if body is equal to an argument, then just print that one
+ if (d_body_argument >= 0)
+ {
+ p->toStreamSygus(out, Node::fromExpr(e[d_body_argument]));
+ }
+ else
+ {
+ // make substitution
+ std::vector<Node> vars;
+ std::vector<Node> subs;
+ for (unsigned i = 0, size = d_args.size(); i < size; i++)
+ {
+ vars.push_back(Node::fromExpr(d_args[i]));
+ std::stringstream ss;
+ ss << "_setpc_var_" << i;
+ Node lv = NodeManager::currentNM()->mkBoundVar(
+ ss.str(), TypeNode::fromType(d_args[i].getType()));
+ subs.push_back(lv);
+ }
+
+ // the substituted body should be a non-sygus term
+ Node sbody = Node::fromExpr(d_body);
+ sbody =
+ sbody.substitute(vars.begin(), vars.end(), subs.begin(), subs.end());
+
+ std::stringstream body_out;
+ body_out << sbody;
+
+ // do string substitution
+ Assert(e.getNumChildren() == d_args.size());
+ std::string str_body = body_out.str();
+ for (unsigned i = 0, size = d_args.size(); i < size; i++)
+ {
+ std::stringstream old_str;
+ old_str << subs[i];
+ std::stringstream new_str;
+ p->toStreamSygus(new_str, Node::fromExpr(e[i]));
+ doStrReplace(str_body, old_str.str().c_str(), new_str.str().c_str());
+ }
+ out << str_body;
+ }
+}
+
+SygusLetExprPrintCallback::SygusLetExprPrintCallback(
+ Expr let_body, std::vector<Expr>& let_args, unsigned ninput_args)
+ : SygusExprPrintCallback(let_body, let_args),
+ d_num_let_input_args(ninput_args)
+{
+}
+
+void SygusLetExprPrintCallback::toStreamSygus(const Printer* p,
+ std::ostream& out,
+ Expr e) const
{
std::stringstream let_out;
// print as let term
- if (d_sygus_num_let_input_args > 0)
+ if (d_num_let_input_args > 0)
{
let_out << "(let (";
}
std::vector<Node> subs_lvs;
std::vector<Node> new_lvs;
- for (unsigned i = 0; i < d_sygus_let_args.size(); i++)
+ for (unsigned i = 0, size = d_args.size(); i < size; i++)
{
- Node v = d_sygus_let_args[i];
+ Node v = d_args[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 < d_sygus_num_let_input_args)
+ if (i < d_num_let_input_args)
{
// it should be printed as a let argument
let_out << "(";
let_out << ")";
}
}
- if (d_sygus_num_let_input_args > 0)
+ if (d_num_let_input_args > 0)
{
let_out << ") ";
}
// print the body
- Node slet_body = d_let_body.substitute(
+ Node slet_body = Node::fromExpr(d_body);
+ slet_body = slet_body.substitute(
subs_lvs.begin(), subs_lvs.end(), new_lvs.begin(), new_lvs.end());
- new_lvs.insert(new_lvs.end(), lvs.begin(), lvs.end());
+ // new_lvs.insert(new_lvs.end(), lvs.begin(), lvs.end());
p->toStreamSygus(let_out, slet_body);
- if (d_sygus_num_let_input_args > 0)
+ if (d_num_let_input_args > 0)
{
let_out << ")";
}
// 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 < d_sygus_let_args.size(); i++)
+ for (unsigned i = 0, size = d_args.size(); i < size; i++)
{
std::stringstream old_str;
old_str << new_lvs[i];
std::stringstream new_str;
- if (i >= d_sygus_num_let_input_args)
+ if (i >= d_num_let_input_args)
{
p->toStreamSygus(new_str, Node::fromExpr(e[i]));
}
else
{
- new_str << d_sygus_let_args[i];
+ new_str << d_args[i];
}
doStrReplace(lbody, old_str.str().c_str(), new_str.str().c_str());
}
out << lbody;
}
-SygusNamedConstructorPrinter::SygusNamedConstructorPrinter(std::string name)
+SygusNamedPrintCallback::SygusNamedPrintCallback(std::string name)
: d_name(name)
{
}
-void SygusNamedConstructorPrinter::toStreamSygus(Printer* p,
- std::ostream& out,
- Expr e)
+void SygusNamedPrintCallback::toStreamSygus(const Printer* p,
+ std::ostream& out,
+ Expr e) const
{
if (e.getNumChildren() > 0)
{
}
}
-void SygusEmptyConstructorPrinter::toStreamSygus(const Printer* p,
- std::ostream& out,
- Expr e)
+void SygusEmptyPrintCallback::toStreamSygus(const Printer* p,
+ std::ostream& out,
+ Expr e) const
{
if (e.getNumChildren() == 1)
{
** \brief sygus print callback functions
**/
-#include "cvc4_private.h"
+#include "cvc4_public.h"
#ifndef __CVC4__PRINTER__SYGUS_PRINT_CALLBACK_H
#define __CVC4__PRINTER__SYGUS_PRINT_CALLBACK_H
#include <vector>
-#include "expr/node.h"
+#include "expr/datatype.h"
+#include "expr/expr.h"
namespace CVC4 {
namespace printer {
+/** sygus expression constructor printer
+ *
+ * This class is used for printing sygus datatype constructor terms whose top
+ * symbol is an expression, such as a custom defined lambda. For example, for
+ * sygus grammar:
+ * A -> (+ x A B) | x | y
+ * B -> 0 | 1
+ * The first constructor, call it C_f for A takes two arguments (A, B) and has
+ * sygus operator
+ * (lambda ((z Int) (w Int)) (+ x z w))
+ * For this operator, we set a print callback that prints, e.g. the term
+ * C_f( t1, t2 )
+ * is printed as:
+ * "(+ x [out1] [out2])"
+ * where out1 is the result of p->toStreamSygus(out,t1) and
+ * out2 is the result of p->toStreamSygus(out,t2).
+ */
+class CVC4_PUBLIC SygusExprPrintCallback : public SygusPrintCallback
+{
+ public:
+ SygusExprPrintCallback(Expr body, std::vector<Expr>& args);
+ ~SygusExprPrintCallback() {}
+ /** print sygus term e on output out using printer p */
+ virtual void toStreamSygus(const Printer* p,
+ std::ostream& out,
+ Expr e) const override;
+
+ protected:
+ /** body of the sygus term */
+ Expr d_body;
+ /** arguments */
+ std::vector<Expr> d_args;
+ /** body argument */
+ int d_body_argument;
+ /** do string replace
+ *
+ * Replaces all occurrences of oldStr with newStr in str.
+ */
+ void doStrReplace(std::string& str,
+ const std::string& oldStr,
+ const std::string& newStr) const;
+};
+
/** sygus let expression constructor printer
*
* This class is used for printing sygus
* A -> (let ((x B)) (+ A 1)) | x | (+ A A) | 0
* B -> 0 | 1
* the first constructor for A takes as arguments
- * (B,A) and has operator
- * (lambda ((y B) (z A)) (+ z 1))
+ * (B,A) and has sygus operator
+ * (lambda ((y Int) (z Int)) (+ z 1))
* CVC4's support for let expressions in grammars
* is highly limited, since notice that the
* argument y : B is unused.
* y is an original input argument of the
* let expression, but z is not.
*/
-class SygusLetExpressionConstructorPrinter
- : public SygusDatatypeConstructorPrinter
+class CVC4_PUBLIC SygusLetExprPrintCallback : public SygusExprPrintCallback
{
public:
- SygusLetExpressionPrinter(Node let_body,
- std::vector<Node>& let_args,
+ SygusLetExprPrintCallback(Expr let_body,
+ std::vector<Expr>& let_args,
unsigned ninput_args);
- ~SygusLetExpressionPrinter() {}
+ ~SygusLetExprPrintCallback() {}
/** print sygus term e on output out using printer p */
virtual void toStreamSygus(const Printer* p,
std::ostream& out,
Expr e) const override;
private:
- /** let body of the sygus term */
- Node d_sygus_let_body;
- /** let arguments */
- std::vector<Node> d_sygus_let_args;
/** number of arguments that are interpreted as input arguments */
- unsigned d_sygus_num_let_input_args;
- /** do string replace
- * Replaces all occurrences of oldStr with newStr in str.
- */
- void doStrReplace(std::string& str,
- const std::string& oldStr,
- const std::string& newStr) const;
+ unsigned d_num_let_input_args;
};
/** sygus named constructor printer
* the first sygus datatype constructor f, where we use
* analog operator (lambda (x) (+ x 1)).
*/
-class SygusNamedConstructorPrinter : public SygusDatatypeConstructorPrinter
+class CVC4_PUBLIC SygusNamedPrintCallback : public SygusPrintCallback
{
public:
- SygusNamedConstructorPrinter(std::string name);
- ~SygusNamedConstructorPrinter() {}
+ SygusNamedPrintCallback(std::string name);
+ ~SygusNamedPrintCallback() {}
/** print sygus term e on output out using printer p */
virtual void toStreamSygus(const Printer* p,
std::ostream& out,
* The first constructor of A, call it cons, has sygus operator (lambda (x) x).
* Call toStreamSygus on cons( t ) should call toStreamSygus on t directly.
*/
-class SygusEmptyConstructorPrinter : public SygusDatatypeConstructorPrinter
+class CVC4_PUBLIC SygusEmptyPrintCallback : public SygusPrintCallback
{
public:
- SygusEmptyConstructorPrinter(std::string name);
- ~SygusEmptyConstructorPrinter() {}
+ SygusEmptyPrintCallback() {}
+ ~SygusEmptyPrintCallback() {}
/** print sygus term e on output out using printer p */
virtual void toStreamSygus(const Printer* p,
std::ostream& out,
#include "theory/quantifiers/ce_guided_conjecture.h"
#include "expr/datatype.h"
+#include "options/base_options.h"
#include "options/quantifiers_options.h"
+#include "printer/printer.h"
#include "prop/prop_engine.h"
#include "smt/smt_statistics_registry.h"
#include "theory/quantifiers/first_order_model.h"
TypeNode tn = nv.getType();
Trace("cegqi-engine") << n[i] << " -> ";
std::stringstream ss;
- std::vector< Node > lvs;
- TermDbSygus::printSygusTerm( ss, nv, lvs );
+ Printer::getPrinter(options::outputLanguage())->toStreamSygus(ss, nv);
Trace("cegqi-engine") << ss.str() << " ";
}
Assert( !nv.isNull() );
if( status==0 ){
out << sol;
}else{
- std::vector< Node > lvs;
- TermDbSygus::printSygusTerm( out, sol, lvs );
+ Printer::getPrinter(options::outputLanguage())->toStreamSygus(out, sol);
}
out << ")" << std::endl;
}
d_sip->debugPrint( "cegqi-si" );
//map from program to bound variables
- std::vector< Node > order_vars;
- std::map< Node, Node > single_inv_app_map;
- for( unsigned j=0; j<progs.size(); j++ ){
- Node prog = progs[j];
- Node pv = d_sip->getFirstOrderVariableForFunction(prog);
- if (!pv.isNull())
- {
- Node inv = d_sip->getFunctionInvocationFor(prog);
- Assert(!inv.isNull());
- single_inv_app_map[prog] = inv;
- Trace("cegqi-si") << " " << pv << ", " << inv << " is associated with program " << prog << std::endl;
- d_prog_to_sol_index[prog] = order_vars.size();
- order_vars.push_back( pv );
- }else{
- Trace("cegqi-si") << " " << prog << " has no fo var." << std::endl;
- }
+ std::vector<Node> funcs;
+ d_sip->getFunctions(funcs);
+ for (unsigned j = 0, size = funcs.size(); j < size; j++)
+ {
+ Assert(std::find(progs.begin(), progs.end(), funcs[j]) != progs.end());
+ d_prog_to_sol_index[funcs[j]] = j;
}
//check if it is single invocation
Trace("cegqi-inv") << " postcondition : " << d_trans_post[prog] << std::endl;
std::vector<Node> sivars;
d_sip->getSingleInvocationVariables(sivars);
- Node invariant = single_inv_app_map[prog];
+ Node invariant = d_sip->getFunctionInvocationFor(prog);
+ Assert(!invariant.isNull());
invariant = invariant.substitute(sivars.begin(),
sivars.end(),
prog_templ_vars.begin(),
struct SynthesisAttributeId {};
typedef expr::Attribute< SynthesisAttributeId, bool > SynthesisAttribute;
+/** Attribute for setting printing information for sygus variables
+ *
+ * For variable d of sygus datatype type, if
+ * d.getAttribute(SygusPrintProxyAttribute) = t, then printing d will print t.
+ */
+struct SygusPrintProxyAttributeId
+{
+};
+typedef expr::Attribute<SygusPrintProxyAttributeId, Node>
+ SygusPrintProxyAttribute;
+
namespace quantifiers {
/** Attribute priority for rewrite rules */
#include "smt/smt_engine.h"
#include "theory/arith/arith_msum.h"
#include "theory/quantifiers/ce_guided_conjecture.h"
+#include "theory/quantifiers/quantifiers_attributes.h"
#include "theory/quantifiers/term_database.h"
#include "theory/quantifiers/term_util.h"
#include "theory/quantifiers/theory_quantifiers.h"
ret = children[0];
}else{
ret = NodeManager::currentNM()->mkNode( ok, children );
- /*
- Node n = NodeManager::currentNM()->mkNode( APPLY, children );
- //must expand definitions
- Node ne = Node::fromExpr( smt::currentSmtEngine()->expandDefinitions( n.toExpr() ) );
- Trace("sygus-db-debug") << "Expanded definitions in " << n << " to " << ne << std::endl;
- return ne;
- */
}
}
Trace("sygus-db-debug") << "...returning " << ret << std::endl;
// if we are not interested in reconstructing constants, or the grammar allows them, return a proxy
if( !options::cegqiSingleInvReconstructConst() || dt.getSygusAllowConst() ){
Node k = NodeManager::currentNM()->mkSkolem( "sy", tn, "sygus proxy" );
- SygusProxyAttribute spa;
+ SygusPrintProxyAttribute spa;
k.setAttribute(spa,c);
sc = k;
}else{
int carg = getOpConsNum( tn, c );
if( carg!=-1 ){
- //sc = Node::fromExpr( dt[carg].getSygusOp() );
sc = NodeManager::currentNM()->mkNode( APPLY_CONSTRUCTOR, Node::fromExpr( dt[carg].getConstructor() ) );
}else{
//identity functions
Kind TermDbSygus::getOperatorKind( Node op ) {
Assert( op.getKind()!=BUILTIN );
- if( smt::currentSmtEngine()->isDefinedFunction( op.toExpr() ) ){
+ Assert(!smt::currentSmtEngine()->isDefinedFunction(op.toExpr()));
+ if (op.getKind() == LAMBDA)
+ {
return APPLY;
}else{
TypeNode tn = op.getType();
if( tn.isConstructor() ){
return APPLY_CONSTRUCTOR;
- }else if( tn.isSelector() ){
+ }
+ else if (tn.isSelector())
+ {
return APPLY_SELECTOR;
- }else if( tn.isTester() ){
+ }
+ else if (tn.isTester())
+ {
return APPLY_TESTER;
- }else{
- return NodeManager::operatorToKind( op );
}
- }
-}
-
-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 << "(";
- }
- 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 << " ";
- printSygusTerm( out, n[i], lvs );
- }
- out << ")";
- }
- }else{
- std::stringstream let_out;
- //print as let term
- if( dt[cIndex].getNumSygusLetInputArgs()>0 ){
- let_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
- let_out << "(";
- let_out << lv << " " << lv.getType() << " ";
- printSygusTerm( let_out, n[i], lvs );
- let_out << ")";
- }
- }
- if( dt[cIndex].getNumSygusLetInputArgs()>0 ){
- 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() );
- 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];
- std::stringstream new_str;
- if( i>=dt[cIndex].getNumSygusLetInputArgs() ){
- printSygusTerm( new_str, n[i], lvs );
- }else{
- new_str << Node::fromExpr( dt[cIndex].getSygusLetArg( i ) );
- }
- doStrReplace( lbody, old_str.str().c_str(), new_str.str().c_str() );
- }
- out << lbody;
- }
- return;
+ else if (tn.isFunction())
+ {
+ return APPLY_UF;
}
- }else if( !n.getAttribute(SygusProxyAttribute()).isNull() ){
- out << n.getAttribute(SygusProxyAttribute());
- }else{
- out << n;
+ return NodeManager::operatorToKind(op);
}
}
/** get operator kind */
static Kind getOperatorKind( Node op );
- /** print sygus term */
- static void printSygusTerm( std::ostream& out, Node n, std::vector< Node >& lvs );
/** get anchor */
static Node getAnchor( Node n );
struct LtePartialInstAttributeId {};
typedef expr::Attribute< LtePartialInstAttributeId, bool > LtePartialInstAttribute;
-// attribute for sygus proxy variables
-struct SygusProxyAttributeId {};
-typedef expr::Attribute<SygusProxyAttributeId, Node> SygusProxyAttribute;
-
// attribute for associating a synthesis function with a first order variable
struct SygusSynthGrammarAttributeId {};
typedef expr::Attribute<SygusSynthGrammarAttributeId, Node>
projects / cvc5.git / commitdiff