diff --git a/proofs/alf/cvc5/Cvc5.smt3 b/proofs/alf/cvc5/Cvc5.smt3 index 639999bad56..2f74a69b498 100644 --- a/proofs/alf/cvc5/Cvc5.smt3 +++ b/proofs/alf/cvc5/Cvc5.smt3 @@ -21,25 +21,6 @@ (declare-sort @ho-elim-sort 1) (declare-const @fmf-fun-sort (-> (! Type :var T :implicit) T Type)) -; side condition for normalizing inputs for the purposes of the reference command -(program parse_normalize ((T Type) (U Type) (S Type) (x T) (y U) (f (-> T S)) (z S)) - (S) S - ( - ((parse_normalize (/ x y)) (let ((xn (parse_normalize x)) (yn (parse_normalize y))) - (let ((xz (alf.to_z xn)) (yz (alf.to_z yn))) - (alf.ite (alf.and (alf.is_eq xz xn) (alf.is_eq yz yn) (alf.not (alf.is_eq yz 0))) - (alf.qdiv xn yn) - (/ xn yn))))) - ((parse_normalize (- x)) (let ((xn (parse_normalize x))) - (let ((xz (alf.to_z xn)) (xq (alf.to_q xn))) - (alf.ite (alf.is_eq xn xz) (alf.neg xn) - (alf.ite (alf.is_eq xn xq) (alf.neg xn) - (- xn)))))) - ((parse_normalize (f x)) (_ (parse_normalize f) (parse_normalize x))) - ((parse_normalize z) z) - ) -) - ; Converts x to an equivalent form, for ProofRule::ENCODE_TRANSFORM. ; This side condition is used to convert between the native ; representation in cvc5 to the form expected by DSL rewrite rules. diff --git a/src/options/printer_options.toml b/src/options/printer_options.toml index 0a473100c6f..bb3ab8caa39 100644 --- a/src/options/printer_options.toml +++ b/src/options/printer_options.toml @@ -63,3 +63,11 @@ name = "Printing" type = "bool" default = "false" help = "print bit-vector constants in decimal (e.g. (_ bv1 4)) instead of binary (e.g. #b0001), applies to SMT-LIB 2.x" + +[[option]] + name = "printArithLitToken" + category = "expert" + long = "print-arith-lit-token" + type = "bool" + default = "false" + help = "print rationals and negative arithmetic literals as lexed tokens, e.g. 1/4, -1.5" diff --git a/src/parser/smt2/smt2_state.cpp b/src/parser/smt2/smt2_state.cpp index 10699439172..1777b0085b1 100644 --- a/src/parser/smt2/smt2_state.cpp +++ b/src/parser/smt2/smt2_state.cpp @@ -1536,31 +1536,10 @@ Term Smt2State::applyParseOp(const ParseOp& p, std::vector& args) } else if (kind == Kind::SUB && args.size() == 1) { - if (isConstInt(args[0]) && args[0].getRealOrIntegerValueSign() > 0) - { - // (- n) denotes a negative value - std::stringstream suminus; - suminus << "-" << args[0].getIntegerValue(); - Term ret = d_tm.mkInteger(suminus.str()); - Trace("parser") << "applyParseOp: return negative constant " << ret - << std::endl; - return ret; - } Term ret = d_tm.mkTerm(Kind::NEG, {args[0]}); Trace("parser") << "applyParseOp: return uminus " << ret << std::endl; return ret; } - else if (kind == Kind::DIVISION && args.size() == 2 && isConstInt(args[0]) - && isConstInt(args[1]) && args[1].getRealOrIntegerValueSign() > 0) - { - // (/ m n) or (/ (- m) n) denote values in reals - std::stringstream sdiv; - sdiv << args[0].getIntegerValue() << "/" << args[1].getIntegerValue(); - Term ret = d_tm.mkReal(sdiv.str()); - Trace("parser") << "applyParseOp: return rational constant " << ret - << std::endl; - return ret; - } else if (kind == Kind::FLOATINGPOINT_FP) { // (fp #bX #bY #bZ) denotes a floating-point value diff --git a/src/printer/smt2/smt2_printer.cpp b/src/printer/smt2/smt2_printer.cpp index 501b9dc95e4..a1792fecad3 100644 --- a/src/printer/smt2/smt2_printer.cpp +++ b/src/printer/smt2/smt2_printer.cpp @@ -73,44 +73,76 @@ static void toStreamRational(std::ostream& out, Variant v) { bool neg = r.sgn() < 0; + bool arithTokens = options::ioutils::getPrintArithLitToken(out); // Print the rational, possibly as a real. // Notice that we print (/ (- 5) 3) instead of (- (/ 5 3)), // the former is compliant with real values in the smt lib standard. if (r.isIntegral()) { - if (neg) + if (arithTokens) { - out << "(- " << -r; + if (neg) + { + out << "-" << -r; + } + else + { + out << r; + } + if (isReal) + { + out << ".0"; + } } else { - out << r; - } - if (isReal) - { - out << ".0"; - } - if (neg) - { - out << ")"; + if (neg) + { + out << "(- " << -r; + } + else + { + out << r; + } + if (isReal) + { + out << ".0"; + } + if (neg) + { + out << ")"; + } } } else { Assert(isReal); - out << "(/ "; - if (neg) + if (arithTokens) { - Rational abs_r = (-r); - out << "(- " << abs_r.getNumerator(); - out << ") " << abs_r.getDenominator(); + if (neg) + { + Rational abs_r = (-r); + out << '-' << abs_r.getNumerator() << '/' << abs_r.getDenominator(); + } + else + { + out << r.getNumerator() << '/' << r.getDenominator(); + } } else { - out << r.getNumerator(); - out << ' ' << r.getDenominator(); + out << "(/ "; + if (neg) + { + Rational abs_r = (-r); + out << "(- " << abs_r.getNumerator() << ") " << abs_r.getDenominator(); + } + else + { + out << r.getNumerator() << ' ' << r.getDenominator(); + } + out << ')'; } - out << ')'; } } diff --git a/src/proof/alf/alf_node_converter.cpp b/src/proof/alf/alf_node_converter.cpp index b2124e1e8e6..2cb05a43e4c 100644 --- a/src/proof/alf/alf_node_converter.cpp +++ b/src/proof/alf/alf_node_converter.cpp @@ -137,29 +137,6 @@ Node AlfNodeConverter::postConvert(Node n) { return mkInternalApp("_", {n[0], n[1]}, tn); } - else if (k == Kind::CONST_INTEGER) - { - Rational r = n.getConst(); - if (r.sgn() == -1) - { - // negative integers are printed as "-n" - std::stringstream ss; - ss << "-" << r.abs(); - return mkInternalSymbol(ss.str(), tn); - } - return n; - } - else if (k == Kind::CONST_RATIONAL) - { - Rational r = n.getConst(); - // ensure rationals are printed properly here using alf syntax, - // which is "n/d" or "-n/d". - Integer num = r.getNumerator().abs(); - Integer den = r.getDenominator(); - std::stringstream ss; - ss << (r.sgn() == -1 ? "-" : "") << num << "/" << den; - return mkInternalSymbol(ss.str(), tn); - } else if (n.isClosure()) { // e.g. (forall ((x1 T1) ... (xn Tk)) P) is diff --git a/src/proof/alf/alf_print_channel.cpp b/src/proof/alf/alf_print_channel.cpp index 80b2f9407f5..3574ad05f4d 100644 --- a/src/proof/alf/alf_print_channel.cpp +++ b/src/proof/alf/alf_print_channel.cpp @@ -72,7 +72,8 @@ void AlfPrintChannelOut::printStepInternal(const std::string& rname, d_out << "(" << (isPop ? "step-pop" : "step") << " @p" << i; if (!n.isNull()) { - printNode(n); + d_out << " "; + printNodeInternal(d_out, n); } d_out << " :rule " << rname; bool firstTime = true; @@ -144,7 +145,6 @@ void AlfPrintChannelOut::printTrustStep(ProofRule r, void AlfPrintChannelOut::printNodeInternal(std::ostream& out, Node n) { - options::ioutils::applyOutputLanguage(out, Language::LANG_SMTLIB_V2_6); if (d_lbind) { // use the toStream with custom letification method @@ -153,13 +153,12 @@ void AlfPrintChannelOut::printNodeInternal(std::ostream& out, Node n) else { // just use default print - out << n; + Printer::getPrinter(out)->toStream(out, n); } } void AlfPrintChannelOut::printTypeNodeInternal(std::ostream& out, TypeNode tn) { - options::ioutils::applyOutputLanguage(out, Language::LANG_SMTLIB_V2_6); tn.toStream(out); } diff --git a/src/proof/alf/alf_printer.cpp b/src/proof/alf/alf_printer.cpp index 8793e1e4195..f678090b351 100644 --- a/src/proof/alf/alf_printer.cpp +++ b/src/proof/alf/alf_printer.cpp @@ -260,6 +260,9 @@ void AlfPrinter::printLetList(std::ostream& out, LetBinding& lbind) void AlfPrinter::print(std::ostream& out, std::shared_ptr pfn) { + // ensures options are set once and for all + options::ioutils::applyOutputLanguage(out, Language::LANG_SMTLIB_V2_6); + options::ioutils::applyPrintArithLitToken(out, true); d_pfIdCounter = 0; // Get the definitions and assertions and print the declarations from them @@ -305,10 +308,10 @@ void AlfPrinter::print(std::ostream& out, std::shared_ptr pfn) } if (options().proof.alfPrintReference) { - // parse_normalize is used as the normalization function for the input // [1] print the reference - out << "(reference \"" << options().driver.filename - << "\" parse_normalize)" << std::endl; + // we currently do not need to provide a normalization routine. + out << "(reference \"" << options().driver.filename << "\")" + << std::endl; // [2] print the universal variables out << outVars.str(); } diff --git a/test/regress/cli/regress0/array-const-real-parse.smt2 b/test/regress/cli/regress0/array-const-real-parse.smt2 index 0246380f8c3..f7336dd9466 100644 --- a/test/regress/cli/regress0/array-const-real-parse.smt2 +++ b/test/regress/cli/regress0/array-const-real-parse.smt2 @@ -1,7 +1,8 @@ +; COMMAND-LINE: --print-arith-lit-token (set-logic QF_AUFLIRA) (set-info :status sat) (declare-fun a () (Array Int Real)) (assert (= a ((as const (Array Int Real)) 0.0))) (declare-fun b () (Array Int Real)) -(assert (= b ((as const (Array Int Real)) (/ 1 3)))) +(assert (= b ((as const (Array Int Real)) 1/3))) (check-sat) diff --git a/test/regress/cli/regress0/arrays/issue7596-define-array-uminus.smt2 b/test/regress/cli/regress0/arrays/issue7596-define-array-uminus.smt2 index da21db28e1b..e4679be98a9 100644 --- a/test/regress/cli/regress0/arrays/issue7596-define-array-uminus.smt2 +++ b/test/regress/cli/regress0/arrays/issue7596-define-array-uminus.smt2 @@ -1,5 +1,6 @@ +; COMMAND-LINE: --print-arith-lit-token (set-logic ALL) (set-info :status sat) -(define-fun foo () (Array Int Int) ((as const (Array Int Int)) (- 1))) +(define-fun foo () (Array Int Int) ((as const (Array Int Int)) -1)) (assert (= (select foo 0) (- 1))) (check-sat)