diff options
Diffstat (limited to 'src/theory/quantifiers/sygus')
13 files changed, 58 insertions, 103 deletions
diff --git a/src/theory/quantifiers/sygus/cegis_core_connective.cpp b/src/theory/quantifiers/sygus/cegis_core_connective.cpp index de75af083..dcdd89c1b 100644 --- a/src/theory/quantifiers/sygus/cegis_core_connective.cpp +++ b/src/theory/quantifiers/sygus/cegis_core_connective.cpp @@ -297,11 +297,10 @@ bool CegisCoreConnective::constructSolution( { Trace("sygus-ccore") << "CegisCoreConnective: Construct candidate solutions..." << std::endl; - Printer* p = Printer::getPrinter(options::outputLanguage()); for (unsigned i = 0, size = candidates.size(); i < size; i++) { std::stringstream ss; - p->toStreamSygus(ss, candidate_values[i]); + TermDbSygus::toStreamSygus(ss, candidate_values[i]); Trace("sygus-ccore") << " " << candidates[i] << " -> " << ss.str() << std::endl; } diff --git a/src/theory/quantifiers/sygus/enum_stream_substitution.cpp b/src/theory/quantifiers/sygus/enum_stream_substitution.cpp index 64e604d0b..91df9d0d6 100644 --- a/src/theory/quantifiers/sygus/enum_stream_substitution.cpp +++ b/src/theory/quantifiers/sygus/enum_stream_substitution.cpp @@ -97,7 +97,7 @@ void EnumStreamPermutation::reset(Node value) for (const Node& var : p.second) { std::stringstream ss; - Printer::getPrinter(options::outputLanguage())->toStreamSygus(ss, var); + TermDbSygus::toStreamSygus(ss, var); Trace("synth-stream-concrete") << " " << ss.str(); } Trace("synth-stream-concrete") << " ]"; @@ -111,7 +111,7 @@ Node EnumStreamPermutation::getNext() if (Trace.isOn("synth-stream-concrete")) { std::stringstream ss; - Printer::getPrinter(options::outputLanguage())->toStreamSygus(ss, d_value); + TermDbSygus::toStreamSygus(ss, d_value); Trace("synth-stream-concrete") << " ....streaming next permutation for value : " << ss.str() << " with " << d_perm_state_class.size() << " permutation classes\n"; @@ -203,8 +203,7 @@ Node EnumStreamPermutation::getNext() if (Trace.isOn("synth-stream-concrete")) { std::stringstream ss; - Printer::getPrinter(options::outputLanguage()) - ->toStreamSygus(ss, perm_value); + TermDbSygus::toStreamSygus(ss, perm_value); Trace("synth-stream-concrete") << " ....return new perm " << ss.str() << "\n"; } @@ -291,8 +290,7 @@ void EnumStreamPermutation::PermutationState::getLastPerm( if (Trace.isOn("synth-stream-concrete")) { std::stringstream ss; - Printer::getPrinter(options::outputLanguage()) - ->toStreamSygus(ss, d_vars[d_last_perm[i]]); + TermDbSygus::toStreamSygus(ss, d_vars[d_last_perm[i]]); Trace("synth-stream-concrete") << " " << ss.str(); } vars.push_back(d_vars[d_last_perm[i]]); @@ -373,7 +371,7 @@ void EnumStreamSubstitution::resetValue(Node value) if (Trace.isOn("synth-stream-concrete")) { std::stringstream ss; - Printer::getPrinter(options::outputLanguage())->toStreamSygus(ss, value); + TermDbSygus::toStreamSygus(ss, value); Trace("synth-stream-concrete") << " * Streaming concrete: registering value " << ss.str() << "\n"; } @@ -402,7 +400,7 @@ void EnumStreamSubstitution::resetValue(Node value) for (const Node& var : p.second) { std::stringstream ss; - Printer::getPrinter(options::outputLanguage())->toStreamSygus(ss, var); + TermDbSygus::toStreamSygus(ss, var); Trace("synth-stream-concrete") << " " << ss.str(); } Trace("synth-stream-concrete") << " ]"; @@ -416,7 +414,7 @@ Node EnumStreamSubstitution::getNext() if (Trace.isOn("synth-stream-concrete")) { std::stringstream ss; - Printer::getPrinter(options::outputLanguage())->toStreamSygus(ss, d_value); + TermDbSygus::toStreamSygus(ss, d_value); Trace("synth-stream-concrete") << " ..streaming next combination of " << ss.str() << "\n"; } @@ -471,7 +469,7 @@ Node EnumStreamSubstitution::getNext() if (Trace.isOn("synth-stream-concrete-debug")) { std::stringstream ss; - Printer::getPrinter(options::outputLanguage())->toStreamSygus(ss, d_last); + TermDbSygus::toStreamSygus(ss, d_last); Trace("synth-stream-concrete-debug") << " ..using base perm " << ss.str() << "\n"; } @@ -521,8 +519,7 @@ Node EnumStreamSubstitution::getNext() if (Trace.isOn("synth-stream-concrete")) { std::stringstream ss; - Printer::getPrinter(options::outputLanguage()) - ->toStreamSygus(ss, comb_value); + TermDbSygus::toStreamSygus(ss, comb_value); Trace("synth-stream-concrete") << " ....register new comb value " << ss.str() << " with rewritten form " << builtin_comb_value @@ -531,20 +528,21 @@ Node EnumStreamSubstitution::getNext() if (!builtin_comb_value.isConst() && !d_comb_values.insert(builtin_comb_value).second) { - std::stringstream ss, ss1; - Printer::getPrinter(options::outputLanguage()) - ->toStreamSygus(ss, comb_value); - Trace("synth-stream-concrete") - << " ..term " << ss.str() << " is REDUNDANT with " << builtin_comb_value - << "\n ..excluding all other concretizations (had " - << d_comb_values.size() << " already)\n\n"; + if (Trace.isOn("synth-stream-concrete")) + { + std::stringstream ss, ss1; + TermDbSygus::toStreamSygus(ss, comb_value); + Trace("synth-stream-concrete") + << " ..term " << ss.str() << " is REDUNDANT with " << builtin_comb_value + << "\n ..excluding all other concretizations (had " + << d_comb_values.size() << " already)\n\n"; + } return Node::null(); } if (Trace.isOn("synth-stream-concrete")) { std::stringstream ss; - Printer::getPrinter(options::outputLanguage()) - ->toStreamSygus(ss, comb_value); + TermDbSygus::toStreamSygus(ss, comb_value); Trace("synth-stream-concrete") << " ..return new comb " << ss.str() << "\n\n"; } @@ -581,8 +579,7 @@ void EnumStreamSubstitution::CombinationState::getLastComb( if (Trace.isOn("synth-stream-concrete")) { std::stringstream ss; - Printer::getPrinter(options::outputLanguage()) - ->toStreamSygus(ss, d_vars[d_last_comb[i]]); + TermDbSygus::toStreamSygus(ss, d_vars[d_last_comb[i]]); Trace("synth-stream-concrete") << " " << ss.str(); } vars.push_back(d_vars[d_last_comb[i]]); diff --git a/src/theory/quantifiers/sygus/sygus_abduct.cpp b/src/theory/quantifiers/sygus/sygus_abduct.cpp index b71a92260..ee37d7b4b 100644 --- a/src/theory/quantifiers/sygus/sygus_abduct.cpp +++ b/src/theory/quantifiers/sygus/sygus_abduct.cpp @@ -19,7 +19,6 @@ #include "expr/dtype.h" #include "expr/node_algorithm.h" #include "expr/sygus_datatype.h" -#include "printer/sygus_print_callback.h" #include "theory/datatypes/sygus_datatype_utils.h" #include "theory/quantifiers/quantifiers_attributes.h" #include "theory/quantifiers/quantifiers_rewriter.h" diff --git a/src/theory/quantifiers/sygus/sygus_grammar_cons.cpp b/src/theory/quantifiers/sygus/sygus_grammar_cons.cpp index cb30a408e..bd5f7ae50 100644 --- a/src/theory/quantifiers/sygus/sygus_grammar_cons.cpp +++ b/src/theory/quantifiers/sygus/sygus_grammar_cons.cpp @@ -18,7 +18,6 @@ #include "expr/datatype.h" #include "options/quantifiers_options.h" -#include "printer/sygus_print_callback.h" #include "theory/bv/theory_bv_utils.h" #include "theory/datatypes/sygus_datatype_utils.h" #include "theory/quantifiers/sygus/sygus_grammar_norm.h" @@ -492,7 +491,7 @@ bool CegGrammarConstructor::isHandledType(TypeNode t) } Node CegGrammarConstructor::createLambdaWithZeroArg( - Kind k, TypeNode bArgType, std::shared_ptr<SygusPrintCallback> spc) + Kind k, TypeNode bArgType) { NodeManager* nm = NodeManager::currentNM(); std::vector<Node> opLArgs; @@ -513,9 +512,6 @@ Node CegGrammarConstructor::createLambdaWithZeroArg( zarg = bv::utils::mkZero(size); } Node body = nm->mkNode(k, zarg, opLArgs.back()); - // use a print callback since we do not want to print the lambda - spc = std::make_shared<printer::SygusExprPrintCallback>(body.toExpr(), - opLArgsExpr); // create operator Node op = nm->mkNode(LAMBDA, nm->mkNode(BOUND_VAR_LIST, opLArgs), body); Trace("sygus-grammar-def") << "\t...building lambda op " << op << "\n"; @@ -1137,15 +1133,6 @@ void CegGrammarConstructor::mkSygusDefaultGrammar( { Node op = nm->mkNode(LAMBDA, nm->mkNode(BOUND_VAR_LIST, opLArgs), monomial); - // use a print callback since we do not want to print the lambda - std::shared_ptr<SygusPrintCallback> spc; - std::vector<Expr> opLArgsExpr; - for (unsigned j = 0, nvars = opLArgs.size(); j < nvars; j++) - { - opLArgsExpr.push_back(opLArgs[j].toExpr()); - } - spc = std::make_shared<printer::SygusExprPrintCallback>( - monomial.toExpr(), opLArgsExpr); // add it as a constructor std::stringstream ssop; ssop << "monomial_" << sdc.d_name; @@ -1153,7 +1140,7 @@ void CegGrammarConstructor::mkSygusDefaultGrammar( // a generalization of a non-Boolean variable (which has weight 0). // This ensures that e.g. ( c1*x >= 0 ) has the same weight as // ( x >= 0 ). - sdts[iat].d_sdt.addConstructor(op, ssop.str(), opCArgs, spc, 0); + sdts[iat].d_sdt.addConstructor(op, ssop.str(), opCArgs, 0); } } if (polynomialGrammar) @@ -1167,14 +1154,6 @@ void CegGrammarConstructor::mkSygusDefaultGrammar( Assert(sumChildren.size() > 1); Node ops = nm->mkNode(PLUS, sumChildren); Node op = nm->mkNode(LAMBDA, nm->mkNode(BOUND_VAR_LIST, lambdaVars), ops); - std::shared_ptr<SygusPrintCallback> spc; - std::vector<Expr> lambdaVarsExpr; - for (unsigned j = 0, nvars = lambdaVars.size(); j < nvars; j++) - { - lambdaVarsExpr.push_back(lambdaVars[j].toExpr()); - } - spc = std::make_shared<printer::SygusExprPrintCallback>(ops.toExpr(), - lambdaVarsExpr); Trace("sygus-grammar-def") << "any term operator is " << op << std::endl; // make the any term datatype, add to back // do not consider the exclusion criteria of the generator @@ -1182,7 +1161,7 @@ void CegGrammarConstructor::mkSygusDefaultGrammar( // a simultaneous generalization of set of non-Boolean variables. // This ensures that ( c1*x + c2*y >= 0 ) has the same weight as // e.g. ( x >= 0 ) or ( y >= 0 ). - sdts[iat].d_sdt.addConstructor(op, "polynomial", cargsAnyTerm, spc, 0); + sdts[iat].d_sdt.addConstructor(op, "polynomial", cargsAnyTerm, 0); // mark that predicates should be of the form (= pol 0) and (<= pol 0) itgat->second.second = true; } @@ -1223,7 +1202,7 @@ void CegGrammarConstructor::mkSygusDefaultGrammar( Trace("sygus-grammar-def") << "...add for variable " << ss.str() << std::endl; std::vector<TypeNode> cargsEmpty; // make boolean variables weight as non-nullary constructors - sdtBool.addConstructor(sygus_vars[i], ss.str(), cargsEmpty, nullptr, 1); + sdtBool.addConstructor(sygus_vars[i], ss.str(), cargsEmpty, 1); } } // add constants @@ -1270,8 +1249,7 @@ void CegGrammarConstructor::mkSygusDefaultGrammar( // predicates if (zarg) { - std::shared_ptr<SygusPrintCallback> spc; - Node op = createLambdaWithZeroArg(k, types[i], spc); + Node op = createLambdaWithZeroArg(k, types[i]); ss << "eq_" << types[i]; sdtBool.addConstructor(op, ss.str(), cargs); } @@ -1283,7 +1261,6 @@ void CegGrammarConstructor::mkSygusDefaultGrammar( cargs.pop_back(); } // type specific predicates - std::shared_ptr<SygusPrintCallback> spc; std::stringstream ssop; if (types[i].isReal()) { @@ -1291,7 +1268,7 @@ void CegGrammarConstructor::mkSygusDefaultGrammar( Trace("sygus-grammar-def") << "...add for " << k << std::endl; if (zarg) { - Node op = createLambdaWithZeroArg(kind, types[i], spc); + Node op = createLambdaWithZeroArg(kind, types[i]); ssop << "leq_" << types[i]; sdtBool.addConstructor(op, ssop.str(), cargs); } @@ -1307,7 +1284,7 @@ void CegGrammarConstructor::mkSygusDefaultGrammar( Trace("sygus-grammar-def") << "...add for " << k << std::endl; if (zarg) { - Node op = createLambdaWithZeroArg(kind, types[i], spc); + Node op = createLambdaWithZeroArg(kind, types[i]); ssop << "leq_" << types[i]; sdtBool.addConstructor(op, ssop.str(), cargs); } @@ -1522,22 +1499,20 @@ void CegGrammarConstructor::SygusDatatypeGenerator::addConstructor( Node op, const std::string& name, const std::vector<TypeNode>& consTypes, - std::shared_ptr<SygusPrintCallback> spc, int weight) { if (shouldInclude(op)) { - d_sdt.addConstructor(op, name, consTypes, spc, weight); + d_sdt.addConstructor(op, name, consTypes, weight); } } void CegGrammarConstructor::SygusDatatypeGenerator::addConstructor( Kind k, const std::vector<TypeNode>& consTypes, - std::shared_ptr<SygusPrintCallback> spc, int weight) { NodeManager* nm = NodeManager::currentNM(); - addConstructor(nm->operatorOf(k), kindToString(k), consTypes, spc, weight); + addConstructor(nm->operatorOf(k), kindToString(k), consTypes, weight); } bool CegGrammarConstructor::SygusDatatypeGenerator::shouldInclude(Node op) const { diff --git a/src/theory/quantifiers/sygus/sygus_grammar_cons.h b/src/theory/quantifiers/sygus/sygus_grammar_cons.h index b0c575809..fd7f84484 100644 --- a/src/theory/quantifiers/sygus/sygus_grammar_cons.h +++ b/src/theory/quantifiers/sygus/sygus_grammar_cons.h @@ -200,7 +200,6 @@ public: void addConstructor(Node op, const std::string& name, const std::vector<TypeNode>& consTypes, - std::shared_ptr<SygusPrintCallback> spc = nullptr, int weight = -1); /** * Possibly add a constructor to d_sdt, based on the criteria mentioned @@ -208,7 +207,6 @@ public: */ void addConstructor(Kind k, const std::vector<TypeNode>& consTypes, - std::shared_ptr<SygusPrintCallback> spc = nullptr, int weight = -1); /** Should we include constructor with operator op? */ bool shouldInclude(Node op) const; @@ -260,13 +258,9 @@ public: * and an extra zero argument of that same type. For example, for k = LEQ and * bArgType = Int, the operator will be lambda x : Int. x + 0. Currently the * supported input types are Real (thus also Int) and BitVector. - * - * This method also creates a print callback for the operator, saved via the - * argument spc, if the caller wishes to not print the lambda. */ static Node createLambdaWithZeroArg(Kind k, - TypeNode bArgType, - std::shared_ptr<SygusPrintCallback> spc); + TypeNode bArgType); //---------------- end grammar construction }; diff --git a/src/theory/quantifiers/sygus/sygus_grammar_norm.cpp b/src/theory/quantifiers/sygus/sygus_grammar_norm.cpp index 819dd6de9..939256b2b 100644 --- a/src/theory/quantifiers/sygus/sygus_grammar_norm.cpp +++ b/src/theory/quantifiers/sygus/sygus_grammar_norm.cpp @@ -18,7 +18,6 @@ #include "expr/datatype.h" #include "expr/node_manager_attributes.h" // for VarNameAttr #include "options/quantifiers_options.h" -#include "printer/sygus_print_callback.h" #include "smt/smt_engine.h" #include "smt/smt_engine_scope.h" #include "theory/datatypes/theory_datatypes_utils.h" @@ -84,8 +83,7 @@ SygusGrammarNorm::TypeObject::TypeObject(TypeNode src_tn, TypeNode unres_tn) void SygusGrammarNorm::TypeObject::addConsInfo( SygusGrammarNorm* sygus_norm, - const DTypeConstructor& cons, - std::shared_ptr<SygusPrintCallback> spc) + const DTypeConstructor& cons) { Trace("sygus-grammar-normalize") << "...for " << cons.getName() << "\n"; /* Recover the sygus operator to not lose reference to the original @@ -107,7 +105,7 @@ void SygusGrammarNorm::TypeObject::addConsInfo( } d_sdt.addConstructor( - sygus_op, cons.getName(), consTypes, spc, cons.getWeight()); + sygus_op, cons.getName(), consTypes, cons.getWeight()); } void SygusGrammarNorm::TypeObject::initializeDatatype( @@ -225,7 +223,6 @@ void SygusGrammarNorm::TransfChain::buildType(SygusGrammarNorm* sygus_norm, to.d_sdt.addConstructor(iden_op, "id", ctypes, - printer::SygusEmptyPrintCallback::getEmptyPC(), 0); Trace("sygus-grammar-normalize-chain") << "\tAdding " << t << " to " << to.d_unres_tn << "\n"; @@ -267,7 +264,6 @@ void SygusGrammarNorm::TransfChain::buildType(SygusGrammarNorm* sygus_norm, to.d_sdt.addConstructor(iden_op, "id_next", ctypes, - printer::SygusEmptyPrintCallback::getEmptyPC(), 0); } @@ -472,7 +468,7 @@ TypeNode SygusGrammarNorm::normalizeSygusRec(TypeNode tn, { unsigned oi = op_pos[i]; Assert(oi < dt.getNumConstructors()); - to.addConsInfo(this, dt[oi], dtt[oi].getSygusPrintCallback()); + to.addConsInfo(this, dt[oi]); } /* Build normalize datatype */ if (Trace.isOn("sygus-grammar-normalize")) diff --git a/src/theory/quantifiers/sygus/sygus_grammar_norm.h b/src/theory/quantifiers/sygus/sygus_grammar_norm.h index 7b635884b..5994d0e7d 100644 --- a/src/theory/quantifiers/sygus/sygus_grammar_norm.h +++ b/src/theory/quantifiers/sygus/sygus_grammar_norm.h @@ -198,8 +198,7 @@ class SygusGrammarNorm * The types of the arguments of "cons" are recursively normalized */ void addConsInfo(SygusGrammarNorm* sygus_norm, - const DTypeConstructor& cons, - std::shared_ptr<SygusPrintCallback> spc); + const DTypeConstructor& cons); /** initializes a datatype with the information in the type object * diff --git a/src/theory/quantifiers/sygus/sygus_interpol.cpp b/src/theory/quantifiers/sygus/sygus_interpol.cpp index 77b193a75..42572a0c7 100644 --- a/src/theory/quantifiers/sygus/sygus_interpol.cpp +++ b/src/theory/quantifiers/sygus/sygus_interpol.cpp @@ -21,7 +21,6 @@ #include "expr/node_algorithm.h" #include "expr/sygus_datatype.h" #include "options/smt_options.h" -#include "printer/sygus_print_callback.h" #include "theory/datatypes/sygus_datatype_utils.h" #include "theory/quantifiers/quantifiers_attributes.h" #include "theory/quantifiers/quantifiers_rewriter.h" diff --git a/src/theory/quantifiers/sygus/sygus_repair_const.cpp b/src/theory/quantifiers/sygus/sygus_repair_const.cpp index cff8f581d..3e632fc56 100644 --- a/src/theory/quantifiers/sygus/sygus_repair_const.cpp +++ b/src/theory/quantifiers/sygus/sygus_repair_const.cpp @@ -129,11 +129,10 @@ bool SygusRepairConst::repairSolution(Node sygusBody, if (Trace.isOn("sygus-repair-const")) { Trace("sygus-repair-const") << "Repair candidate solutions..." << std::endl; - Printer* p = Printer::getPrinter(options::outputLanguage()); for (unsigned i = 0, size = candidates.size(); i < size; i++) { std::stringstream ss; - p->toStreamSygus(ss, candidate_values[i]); + TermDbSygus::toStreamSygus(ss, candidate_values[i]); Trace("sygus-repair-const") << " " << candidates[i] << " -> " << ss.str() << std::endl; } @@ -151,9 +150,8 @@ bool SygusRepairConst::repairSolution(Node sygusBody, cv, free_var_count, sk_vars, sk_vars_to_subs, useConstantsAsHoles); if (Trace.isOn("sygus-repair-const")) { - Printer* p = Printer::getPrinter(options::outputLanguage()); std::stringstream ss; - p->toStreamSygus(ss, cv); + TermDbSygus::toStreamSygus(ss, cv); Trace("sygus-repair-const") << "Solution #" << i << " : " << ss.str() << std::endl; if (skeleton == cv) @@ -163,7 +161,7 @@ bool SygusRepairConst::repairSolution(Node sygusBody, else { std::stringstream sss; - p->toStreamSygus(sss, skeleton); + TermDbSygus::toStreamSygus(sss, skeleton); Trace("sygus-repair-const") << "...inferred skeleton : " << sss.str() << std::endl; } @@ -269,8 +267,7 @@ bool SygusRepairConst::repairSolution(Node sygusBody, if (Trace.isOn("sygus-repair-const") || Trace.isOn("sygus-engine")) { std::stringstream sss; - Printer::getPrinter(options::outputLanguage()) - ->toStreamSygus(sss, repair_cv[i]); + TermDbSygus::toStreamSygus(sss, repair_cv[i]); ss << " * " << candidates[i] << " -> " << sss.str() << std::endl; } } diff --git a/src/theory/quantifiers/sygus/sygus_unif_rl.cpp b/src/theory/quantifiers/sygus/sygus_unif_rl.cpp index 9fb0702b1..86cb69f48 100644 --- a/src/theory/quantifiers/sygus/sygus_unif_rl.cpp +++ b/src/theory/quantifiers/sygus/sygus_unif_rl.cpp @@ -713,8 +713,7 @@ Node SygusUnifRl::DecisionTreeInfo::buildSolMinCond(Node cons, if (Trace.isOn("sygus-unif-sol")) { std::stringstream ss; - Printer::getPrinter(options::outputLanguage()) - ->toStreamSygus(ss, hd_mv[e]); + TermDbSygus::toStreamSygus(ss, hd_mv[e]); Trace("sygus-unif-sol") << " add evaluation head (" << hd_counter << "/" << d_hds.size() << "): " << e << " -> " << ss.str() << std::endl; @@ -766,7 +765,7 @@ Node SygusUnifRl::DecisionTreeInfo::buildSolMinCond(Node cons, if (Trace.isOn("sygus-unif-sol")) { std::stringstream ss; - Printer::getPrinter(options::outputLanguage())->toStreamSygus(ss, cv); + TermDbSygus::toStreamSygus(ss, cv); Trace("sygus-unif-sol") << " add condition (" << c_counter << "/" << d_conds.size() << "): " << ce << " -> " << ss.str() << std::endl; diff --git a/src/theory/quantifiers/sygus/synth_conjecture.cpp b/src/theory/quantifiers/sygus/synth_conjecture.cpp index 6ade49b6d..9608de743 100644 --- a/src/theory/quantifiers/sygus/synth_conjecture.cpp +++ b/src/theory/quantifiers/sygus/synth_conjecture.cpp @@ -373,7 +373,7 @@ bool SynthConjecture::doCheck(std::vector<Node>& lems) for (const Node& fc : fail_cvs) { std::stringstream ss; - Printer::getPrinter(options::outputLanguage())->toStreamSygus(ss, fc); + TermDbSygus::toStreamSygus(ss, fc); Trace("sygus-engine") << ss.str() << " "; } Trace("sygus-engine") << std::endl; @@ -434,7 +434,7 @@ bool SynthConjecture::doCheck(std::vector<Node>& lems) Node onv = nv.isNull() ? d_qe->getModel()->getValue(terms[i]) : nv; TypeNode tn = onv.getType(); std::stringstream ss; - Printer::getPrinter(options::outputLanguage())->toStreamSygus(ss, onv); + TermDbSygus::toStreamSygus(ss, onv); if (printDebug) { sygusEnumOut << " " << ss.str(); @@ -559,7 +559,7 @@ bool SynthConjecture::doCheck(std::vector<Node>& lems) { Node v = candidate_values[i]; std::stringstream ss; - Printer::getPrinter(options::outputLanguage())->toStreamSygus(ss, v); + TermDbSygus::toStreamSygus(ss, v); out << "(" << d_quant[0][i] << " " << ss.str() << ")"; } out << ")" << std::endl; @@ -1193,8 +1193,8 @@ void SynthConjecture::printSynthSolution(std::ostream& out) } else { - Printer::getPrinter(options::outputLanguage()) - ->toStreamSygus(out, sol); + Node bsol = datatypes::utils::sygusToBuiltin(sol, true); + out << bsol; } out << ")" << std::endl; } diff --git a/src/theory/quantifiers/sygus/term_database_sygus.cpp b/src/theory/quantifiers/sygus/term_database_sygus.cpp index ac1c7d342..c2a02e715 100644 --- a/src/theory/quantifiers/sygus/term_database_sygus.cpp +++ b/src/theory/quantifiers/sygus/term_database_sygus.cpp @@ -723,19 +723,18 @@ void TermDbSygus::toStreamSygus(const char* c, Node n) { if (Trace.isOn(c)) { - if (n.isNull()) - { - Trace(c) << n; - } - else - { - std::stringstream ss; - Printer::getPrinter(options::outputLanguage())->toStreamSygus(ss, n); - Trace(c) << ss.str(); - } + std::stringstream ss; + toStreamSygus(ss, n); + Trace(c) << ss.str(); } } +void TermDbSygus::toStreamSygus(std::ostream& out, Node n) +{ + // use external conversion + out << datatypes::utils::sygusToBuiltin(n, true); +} + SygusTypeInfo& TermDbSygus::getTypeInfo(TypeNode tn) { AlwaysAssert(d_tinfo.find(tn) != d_tinfo.end()); diff --git a/src/theory/quantifiers/sygus/term_database_sygus.h b/src/theory/quantifiers/sygus/term_database_sygus.h index 97cdc6ddd..921b08de5 100644 --- a/src/theory/quantifiers/sygus/term_database_sygus.h +++ b/src/theory/quantifiers/sygus/term_database_sygus.h @@ -310,7 +310,9 @@ class TermDbSygus { /** print to sygus stream n on trace c */ static void toStreamSygus(const char* c, Node n); - + /** print to sygus stream n on output out */ + static void toStreamSygus(std::ostream& out, Node n); + private: /** reference to the quantifiers engine */ QuantifiersEngine* d_quantEngine; |