From 528e801343c692b0ce8123f8754e069e6523f5dc Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Fri, 14 Feb 2020 17:09:59 -0600 Subject: [PATCH] Remove quantifiers rewrite rules infrastructure (#3754) --- src/CMakeLists.txt | 2 - src/api/cvc4cppkind.h | 8 - src/bindings/java/CMakeLists.txt | 2 - src/options/quantifiers_options.toml | 9 - src/parser/smt2/Smt2.g | 95 +--- src/parser/smt2/smt2.cpp | 27 - src/parser/smt2/smt2.h | 18 - src/smt/command.cpp | 247 --------- src/smt/command.h | 74 --- src/smt/smt_engine.cpp | 6 - src/theory/quantifiers/kinds | 21 - .../quantifiers/quantifiers_attributes.cpp | 40 -- .../quantifiers/quantifiers_attributes.h | 12 - .../quantifiers/quantifiers_rewriter.cpp | 133 +---- src/theory/quantifiers/quantifiers_rewriter.h | 1 - src/theory/quantifiers/rewrite_engine.cpp | 309 ----------- src/theory/quantifiers/rewrite_engine.h | 86 --- .../theory_quantifiers_type_rules.h | 85 --- src/theory/quantifiers_engine.cpp | 21 +- src/theory/term_registration_visitor.cpp | 4 +- test/regress/CMakeLists.txt | 35 -- .../regress0/rewriterules/datatypes.smt2 | 102 ---- .../rewriterules/datatypes_clark.smt2 | 205 -------- .../regress/regress0/rewriterules/length.smt2 | 27 - .../regress0/rewriterules/length_gen_n.smt2 | 46 -- .../rewriterules/length_gen_n_lemma.smt2 | 44 -- .../regress0/rewriterules/length_trick.smt2 | 33 -- .../regress0/rewriterules/length_trick2.smt2 | 33 -- .../regress0/rewriterules/native_arrays.smt2 | 35 -- .../rewriterules/native_datatypes.smt2 | 34 -- .../regress0/rewriterules/relation.smt2 | 28 - .../rewriterules/simulate_rewriting.smt2 | 25 - test/regress/regress1/push-pop/bug326.smt2 | 41 -- .../regress1/rewriterules/datatypes2.smt2 | 151 ------ .../regress1/rewriterules/datatypes3.smt2 | 138 ----- .../datatypes_clark_quantification.smt2 | 265 ---------- .../regress1/rewriterules/datatypes_sat.smt2 | 102 ---- .../regress1/rewriterules/length_gen.smt2 | 35 -- .../regress1/rewriterules/length_gen_010.smt2 | 37 -- .../rewriterules/length_gen_010_lemma.smt2 | 35 -- .../regress1/rewriterules/length_gen_020.smt2 | 35 -- .../rewriterules/length_gen_020_sat.smt2 | 35 -- .../regress1/rewriterules/length_gen_040.smt2 | 35 -- .../rewriterules/length_gen_040_lemma.smt2 | 35 -- .../length_gen_040_lemma_trigger.smt2 | 36 -- .../regress1/rewriterules/length_gen_080.smt2 | 35 -- .../rewriterules/length_gen_160_lemma.smt2 | 35 -- .../rewriterules/length_gen_inv_160.smt2 | 35 -- .../regress1/rewriterules/length_trick3.smt2 | 37 -- .../rewriterules/length_trick3_int.smt2 | 45 -- .../reachability_back_to_the_future.smt2 | 55 -- test/regress/regress1/rewriterules/read5.smt2 | 36 -- .../set_A_new_fast_tableau-base.smt2 | 127 ----- .../set_A_new_fast_tableau-base_sat.smt2 | 128 ----- .../regress1/rewriterules/test_guards.smt2 | 46 -- .../why3_vstte10_max_sum_harness2.smt2 | 493 ------------------ 56 files changed, 25 insertions(+), 3874 deletions(-) delete mode 100644 src/theory/quantifiers/rewrite_engine.cpp delete mode 100644 src/theory/quantifiers/rewrite_engine.h delete mode 100644 test/regress/regress0/rewriterules/datatypes.smt2 delete mode 100644 test/regress/regress0/rewriterules/datatypes_clark.smt2 delete mode 100644 test/regress/regress0/rewriterules/length.smt2 delete mode 100644 test/regress/regress0/rewriterules/length_gen_n.smt2 delete mode 100644 test/regress/regress0/rewriterules/length_gen_n_lemma.smt2 delete mode 100644 test/regress/regress0/rewriterules/length_trick.smt2 delete mode 100644 test/regress/regress0/rewriterules/length_trick2.smt2 delete mode 100644 test/regress/regress0/rewriterules/native_arrays.smt2 delete mode 100644 test/regress/regress0/rewriterules/native_datatypes.smt2 delete mode 100644 test/regress/regress0/rewriterules/relation.smt2 delete mode 100644 test/regress/regress0/rewriterules/simulate_rewriting.smt2 delete mode 100644 test/regress/regress1/push-pop/bug326.smt2 delete mode 100644 test/regress/regress1/rewriterules/datatypes2.smt2 delete mode 100644 test/regress/regress1/rewriterules/datatypes3.smt2 delete mode 100644 test/regress/regress1/rewriterules/datatypes_clark_quantification.smt2 delete mode 100644 test/regress/regress1/rewriterules/datatypes_sat.smt2 delete mode 100644 test/regress/regress1/rewriterules/length_gen.smt2 delete mode 100644 test/regress/regress1/rewriterules/length_gen_010.smt2 delete mode 100644 test/regress/regress1/rewriterules/length_gen_010_lemma.smt2 delete mode 100644 test/regress/regress1/rewriterules/length_gen_020.smt2 delete mode 100644 test/regress/regress1/rewriterules/length_gen_020_sat.smt2 delete mode 100644 test/regress/regress1/rewriterules/length_gen_040.smt2 delete mode 100644 test/regress/regress1/rewriterules/length_gen_040_lemma.smt2 delete mode 100644 test/regress/regress1/rewriterules/length_gen_040_lemma_trigger.smt2 delete mode 100644 test/regress/regress1/rewriterules/length_gen_080.smt2 delete mode 100644 test/regress/regress1/rewriterules/length_gen_160_lemma.smt2 delete mode 100644 test/regress/regress1/rewriterules/length_gen_inv_160.smt2 delete mode 100644 test/regress/regress1/rewriterules/length_trick3.smt2 delete mode 100644 test/regress/regress1/rewriterules/length_trick3_int.smt2 delete mode 100644 test/regress/regress1/rewriterules/reachability_back_to_the_future.smt2 delete mode 100644 test/regress/regress1/rewriterules/read5.smt2 delete mode 100644 test/regress/regress1/rewriterules/set_A_new_fast_tableau-base.smt2 delete mode 100644 test/regress/regress1/rewriterules/set_A_new_fast_tableau-base_sat.smt2 delete mode 100644 test/regress/regress1/rewriterules/test_guards.smt2 delete mode 100644 test/regress/regress1/rewriterules/why3_vstte10_max_sum_harness2.smt2 diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt index 975dd26f6..871cb2f99 100644 --- a/src/CMakeLists.txt +++ b/src/CMakeLists.txt @@ -544,8 +544,6 @@ libcvc4_add_sources( theory/quantifiers/query_generator.h theory/quantifiers/relevant_domain.cpp theory/quantifiers/relevant_domain.h - theory/quantifiers/rewrite_engine.cpp - theory/quantifiers/rewrite_engine.h theory/quantifiers/single_inv_partition.cpp theory/quantifiers/single_inv_partition.h theory/quantifiers/skolemize.cpp diff --git a/src/api/cvc4cppkind.h b/src/api/cvc4cppkind.h index bb2700706..2242c8e00 100644 --- a/src/api/cvc4cppkind.h +++ b/src/api/cvc4cppkind.h @@ -2181,14 +2181,6 @@ enum CVC4_PUBLIC Kind : int32_t INST_PATTERN_LIST, /* predicate for specifying term in instantiation closure. */ INST_CLOSURE, - /* general rewrite rule (for rewrite-rules theory) */ - REWRITE_RULE, - /* actual rewrite rule (for rewrite-rules theory) */ - RR_REWRITE, - /* actual reduction rule (for rewrite-rules theory) */ - RR_REDUCTION, - /* actual deduction rule (for rewrite-rules theory) */ - RR_DEDUCTION, /* Sort Kinds ------------------------------------------------------------ */ diff --git a/src/bindings/java/CMakeLists.txt b/src/bindings/java/CMakeLists.txt index 3cd6a7e51..7c2985e5c 100644 --- a/src/bindings/java/CMakeLists.txt +++ b/src/bindings/java/CMakeLists.txt @@ -160,7 +160,6 @@ set(gen_java_files ${CMAKE_CURRENT_BINARY_DIR}/PopCommand.java ${CMAKE_CURRENT_BINARY_DIR}/PrettySExprs.java ${CMAKE_CURRENT_BINARY_DIR}/Proof.java - ${CMAKE_CURRENT_BINARY_DIR}/PropagateRuleCommand.java ${CMAKE_CURRENT_BINARY_DIR}/PushCommand.java ${CMAKE_CURRENT_BINARY_DIR}/QueryCommand.java ${CMAKE_CURRENT_BINARY_DIR}/QuitCommand.java @@ -177,7 +176,6 @@ set(gen_java_files ${CMAKE_CURRENT_BINARY_DIR}/ResetCommand.java ${CMAKE_CURRENT_BINARY_DIR}/ResourceManager.java ${CMAKE_CURRENT_BINARY_DIR}/Result.java - ${CMAKE_CURRENT_BINARY_DIR}/RewriteRuleCommand.java ${CMAKE_CURRENT_BINARY_DIR}/RoundingMode.java ${CMAKE_CURRENT_BINARY_DIR}/RoundingModeType.java ${CMAKE_CURRENT_BINARY_DIR}/SExpr.java diff --git a/src/options/quantifiers_options.toml b/src/options/quantifiers_options.toml index 908846bea..84545e66e 100644 --- a/src/options/quantifiers_options.toml +++ b/src/options/quantifiers_options.toml @@ -898,15 +898,6 @@ header = "options/quantifiers_options.h" ### Rewrite rules options -[[option]] - name = "quantRewriteRules" - category = "regular" - long = "rewrite-rules" - type = "bool" - default = "false" - read_only = true - help = "use rewrite rules module" - [[option]] name = "rrOneInstPerRound" category = "regular" diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g index aed62f94c..90303dd40 100644 --- a/src/parser/smt2/Smt2.g +++ b/src/parser/smt2/Smt2.g @@ -1254,8 +1254,6 @@ extendedCommand[std::unique_ptr* cmd] | DECLARE_CODATATYPES_2_5_TOK datatypes_2_5_DefCommand[true, cmd] | DECLARE_CODATATYPE_TOK datatypeDefCommand[true, cmd] | DECLARE_CODATATYPES_TOK datatypesDefCommand[true, cmd] - | rewriterulesCommand[cmd] - /* Support some of Z3's extended SMT-LIB commands */ | DECLARE_SORTS_TOK { PARSER_STATE->checkThatLogicIsSet(); } @@ -1545,43 +1543,6 @@ datatypesDef[bool isCo, } ; -rewriterulesCommand[std::unique_ptr* cmd] -@declarations { - std::vector guards, heads, triggers; - Expr head, body, bvl, expr, expr2; - Kind kind; -} - : /* rewrite rules */ - REWRITE_RULE_TOK { kind = CVC4::kind::RR_REWRITE; } - { PARSER_STATE->pushScope(true); } - boundVarList[bvl] - LPAREN_TOK ( pattern[expr] { triggers.push_back( expr ); } )* RPAREN_TOK - LPAREN_TOK (termList[guards,expr])? RPAREN_TOK - term[head, expr2] - term[body, expr2] - { - *cmd = PARSER_STATE->assertRewriteRule( - kind, bvl, triggers, guards, {head}, body); - } - /* propagation rule */ - | rewritePropaKind[kind] - { PARSER_STATE->pushScope(true); } - boundVarList[bvl] - LPAREN_TOK ( pattern[expr] { triggers.push_back( expr ); } )* RPAREN_TOK - LPAREN_TOK (termList[guards,expr])? RPAREN_TOK - LPAREN_TOK (termList[heads,expr])? RPAREN_TOK - term[body, expr2] - { - *cmd = PARSER_STATE->assertRewriteRule( - kind, bvl, triggers, guards, heads, body); - } - ; - -rewritePropaKind[CVC4::Kind& kind] - : REDUCTION_RULE_TOK { $kind = CVC4::kind::RR_REDUCTION; } - | PROPAGATION_RULE_TOK { $kind = CVC4::kind::RR_DEDUCTION; } - ; - pattern[CVC4::Expr& expr] @declarations { std::vector patexpr; @@ -1631,8 +1592,7 @@ simpleSymbolicExprNoKeyword[CVC4::SExpr& sexpr] | GET_UNSAT_CORE_TOK | EXIT_TOK | RESET_TOK | RESET_ASSERTIONS_TOK | SET_LOGIC_TOK | SET_INFO_TOK | GET_INFO_TOK | SET_OPTION_TOK | GET_OPTION_TOK | PUSH_TOK | POP_TOK - | DECLARE_DATATYPES_TOK | GET_MODEL_TOK | ECHO_TOK | REWRITE_RULE_TOK - | REDUCTION_RULE_TOK | PROPAGATION_RULE_TOK | SIMPLIFY_TOK) + | DECLARE_DATATYPES_TOK | GET_MODEL_TOK | ECHO_TOK | SIMPLIFY_TOK) { sexpr = SExpr(SExpr::Keyword(AntlrInput::tokenText($tok))); } ; @@ -1713,25 +1673,11 @@ termNonVariable[CVC4::Expr& expr, CVC4::Expr& expr2] args.push_back(bvl); PARSER_STATE->popScope(); - switch(f.getKind()) { - case CVC4::kind::RR_REWRITE: - case CVC4::kind::RR_REDUCTION: - case CVC4::kind::RR_DEDUCTION: - if(kind == CVC4::kind::EXISTS) { - PARSER_STATE->parseError("Use Exists instead of Forall for a rewrite " - "rule."); - } - args.push_back(f2); // guards - args.push_back(f); // rule - expr = MK_EXPR(CVC4::kind::REWRITE_RULE, args); - break; - default: - args.push_back(f); - if(! f2.isNull()){ - args.push_back(f2); - } - expr = MK_EXPR(kind, args); + args.push_back(f); + if(! f2.isNull()){ + args.push_back(f2); } + expr = MK_EXPR(kind, args); } | LPAREN_TOK COMPREHENSION_TOK { PARSER_STATE->pushScope(true); } @@ -1902,33 +1848,7 @@ termNonVariable[CVC4::Expr& expr, CVC4::Expr& expr2] } )+ RPAREN_TOK { - if(attr == ":rewrite-rule") { - Expr guard; - Expr body; - if(expr[1].getKind() == kind::IMPLIES || - expr[1].getKind() == kind::EQUAL) { - guard = expr[0]; - body = expr[1]; - } else { - guard = MK_CONST(bool(true)); - body = expr; - } - expr2 = guard; - args.push_back(body[0]); - args.push_back(body[1]); - if(!f2.isNull()) { - args.push_back(f2); - } - - if( body.getKind()==kind::IMPLIES ){ - kind = kind::RR_DEDUCTION; - }else if( body.getKind()==kind::EQUAL ){ - kind = body[0].getType().isBoolean() ? kind::RR_REDUCTION : kind::RR_REWRITE; - }else{ - PARSER_STATE->parseError("Error parsing rewrite rule."); - } - expr = MK_EXPR( kind, args ); - } else if(! patexprs.empty()) { + if(! patexprs.empty()) { if( !f2.isNull() && f2.getKind()==kind::INST_PATTERN_LIST ){ for( size_t i=0; i Smt2::assertRewriteRule( - Kind kind, - Expr bvl, - const std::vector& triggers, - const std::vector& guards, - const std::vector& heads, - Expr body) -{ - assert(kind == kind::RR_REWRITE || kind == kind::RR_REDUCTION - || kind == kind::RR_DEDUCTION); - - ExprManager* em = getExprManager(); - - std::vector args; - args.push_back(mkAnd(heads)); - args.push_back(body); - - if (!triggers.empty()) - { - args.push_back(em->mkExpr(kind::INST_PATTERN_LIST, triggers)); - } - - Expr rhs = em->mkExpr(kind, args); - Expr rule = em->mkExpr(kind::REWRITE_RULE, bvl, mkAnd(guards), rhs); - return std::unique_ptr(new AssertCommand(rule, false)); -} - Smt2::SynthFunFactory::SynthFunFactory( Smt2* smt2, const std::string& fun, diff --git a/src/parser/smt2/smt2.h b/src/parser/smt2/smt2.h index 6c1275115..6427b32d5 100644 --- a/src/parser/smt2/smt2.h +++ b/src/parser/smt2/smt2.h @@ -197,24 +197,6 @@ class Smt2 : public Parser void resetAssertions(); - /** - * Creates a command that asserts a rule. - * - * @param kind The kind of rule (RR_REWRITE, RR_REDUCTION, RR_DEDUCTION) - * @param bvl Bound variable list - * @param triggers List of triggers - * @param guards List of guards - * @param heads List of heads - * @param body The body of the rule - * @return The command that asserts the rewrite rule - */ - std::unique_ptr assertRewriteRule(Kind kind, - Expr bvl, - const std::vector& triggers, - const std::vector& guards, - const std::vector& heads, - Expr body); - /** * Class for creating instances of `SynthFunCommand`s. Creating an instance * of this class pushes the scope, destroying it pops the scope. diff --git a/src/smt/command.cpp b/src/smt/command.cpp index 17d8cbed5..ce8d4fa88 100644 --- a/src/smt/command.cpp +++ b/src/smt/command.cpp @@ -2841,251 +2841,4 @@ std::string DatatypeDeclarationCommand::getCommandName() const return "declare-datatypes"; } -/* -------------------------------------------------------------------------- */ -/* class RewriteRuleCommand */ -/* -------------------------------------------------------------------------- */ - -RewriteRuleCommand::RewriteRuleCommand(const std::vector& vars, - const std::vector& guards, - Expr head, - Expr body, - const Triggers& triggers) - : d_vars(vars), - d_guards(guards), - d_head(head), - d_body(body), - d_triggers(triggers) -{ -} - -RewriteRuleCommand::RewriteRuleCommand(const std::vector& vars, - Expr head, - Expr body) - : d_vars(vars), d_head(head), d_body(body) -{ -} - -const std::vector& RewriteRuleCommand::getVars() const { return d_vars; } -const std::vector& RewriteRuleCommand::getGuards() const -{ - return d_guards; -} - -Expr RewriteRuleCommand::getHead() const { return d_head; } -Expr RewriteRuleCommand::getBody() const { return d_body; } -const RewriteRuleCommand::Triggers& RewriteRuleCommand::getTriggers() const -{ - return d_triggers; -} - -void RewriteRuleCommand::invoke(SmtEngine* smtEngine) -{ - try - { - ExprManager* em = smtEngine->getExprManager(); - /** build vars list */ - Expr vars = em->mkExpr(kind::BOUND_VAR_LIST, d_vars); - /** build guards list */ - Expr guards; - if (d_guards.size() == 0) - guards = em->mkConst(true); - else if (d_guards.size() == 1) - guards = d_guards[0]; - else - guards = em->mkExpr(kind::AND, d_guards); - /** build expression */ - Expr expr; - if (d_triggers.empty()) - { - expr = em->mkExpr(kind::RR_REWRITE, vars, guards, d_head, d_body); - } - else - { - /** build triggers list */ - std::vector vtriggers; - vtriggers.reserve(d_triggers.size()); - for (Triggers::const_iterator i = d_triggers.begin(), - end = d_triggers.end(); - i != end; - ++i) - { - vtriggers.push_back(em->mkExpr(kind::INST_PATTERN, *i)); - } - Expr triggers = em->mkExpr(kind::INST_PATTERN_LIST, vtriggers); - expr = - em->mkExpr(kind::RR_REWRITE, vars, guards, d_head, d_body, triggers); - } - smtEngine->assertFormula(expr); - d_commandStatus = CommandSuccess::instance(); - } - catch (exception& e) - { - d_commandStatus = new CommandFailure(e.what()); - } -} - -Command* RewriteRuleCommand::exportTo(ExprManager* exprManager, - ExprManagerMapCollection& variableMap) -{ - /** Convert variables */ - VExpr vars = ExportTo(exprManager, variableMap, d_vars); - /** Convert guards */ - VExpr guards = ExportTo(exprManager, variableMap, d_guards); - /** Convert triggers */ - Triggers triggers; - triggers.reserve(d_triggers.size()); - for (const std::vector& trigger_list : d_triggers) - { - triggers.push_back(ExportTo(exprManager, variableMap, trigger_list)); - } - /** Convert head and body */ - Expr head = d_head.exportTo(exprManager, variableMap); - Expr body = d_body.exportTo(exprManager, variableMap); - /** Create the converted rules */ - return new RewriteRuleCommand(vars, guards, head, body, triggers); -} - -Command* RewriteRuleCommand::clone() const -{ - return new RewriteRuleCommand(d_vars, d_guards, d_head, d_body, d_triggers); -} - -std::string RewriteRuleCommand::getCommandName() const -{ - return "rewrite-rule"; -} - -/* -------------------------------------------------------------------------- */ -/* class PropagateRuleCommand */ -/* -------------------------------------------------------------------------- */ - -PropagateRuleCommand::PropagateRuleCommand(const std::vector& vars, - const std::vector& guards, - const std::vector& heads, - Expr body, - const Triggers& triggers, - bool deduction) - : d_vars(vars), - d_guards(guards), - d_heads(heads), - d_body(body), - d_triggers(triggers), - d_deduction(deduction) -{ -} - -PropagateRuleCommand::PropagateRuleCommand(const std::vector& vars, - const std::vector& heads, - Expr body, - bool deduction) - : d_vars(vars), d_heads(heads), d_body(body), d_deduction(deduction) -{ -} - -const std::vector& PropagateRuleCommand::getVars() const -{ - return d_vars; -} - -const std::vector& PropagateRuleCommand::getGuards() const -{ - return d_guards; -} - -const std::vector& PropagateRuleCommand::getHeads() const -{ - return d_heads; -} - -Expr PropagateRuleCommand::getBody() const { return d_body; } -const PropagateRuleCommand::Triggers& PropagateRuleCommand::getTriggers() const -{ - return d_triggers; -} - -bool PropagateRuleCommand::isDeduction() const { return d_deduction; } -void PropagateRuleCommand::invoke(SmtEngine* smtEngine) -{ - try - { - ExprManager* em = smtEngine->getExprManager(); - /** build vars list */ - Expr vars = em->mkExpr(kind::BOUND_VAR_LIST, d_vars); - /** build guards list */ - Expr guards; - if (d_guards.size() == 0) - guards = em->mkConst(true); - else if (d_guards.size() == 1) - guards = d_guards[0]; - else - guards = em->mkExpr(kind::AND, d_guards); - /** build heads list */ - Expr heads; - if (d_heads.size() == 1) - heads = d_heads[0]; - else - heads = em->mkExpr(kind::AND, d_heads); - /** build expression */ - Expr expr; - if (d_triggers.empty()) - { - expr = em->mkExpr(kind::RR_REWRITE, vars, guards, heads, d_body); - } - else - { - /** build triggers list */ - std::vector vtriggers; - vtriggers.reserve(d_triggers.size()); - for (Triggers::const_iterator i = d_triggers.begin(), - end = d_triggers.end(); - i != end; - ++i) - { - vtriggers.push_back(em->mkExpr(kind::INST_PATTERN, *i)); - } - Expr triggers = em->mkExpr(kind::INST_PATTERN_LIST, vtriggers); - expr = - em->mkExpr(kind::RR_REWRITE, vars, guards, heads, d_body, triggers); - } - smtEngine->assertFormula(expr); - d_commandStatus = CommandSuccess::instance(); - } - catch (exception& e) - { - d_commandStatus = new CommandFailure(e.what()); - } -} - -Command* PropagateRuleCommand::exportTo(ExprManager* exprManager, - ExprManagerMapCollection& variableMap) -{ - /** Convert variables */ - VExpr vars = ExportTo(exprManager, variableMap, d_vars); - /** Convert guards */ - VExpr guards = ExportTo(exprManager, variableMap, d_guards); - /** Convert heads */ - VExpr heads = ExportTo(exprManager, variableMap, d_heads); - /** Convert triggers */ - Triggers triggers; - triggers.reserve(d_triggers.size()); - for (const std::vector& trigger_list : d_triggers) - { - triggers.push_back(ExportTo(exprManager, variableMap, trigger_list)); - } - /** Convert head and body */ - Expr body = d_body.exportTo(exprManager, variableMap); - /** Create the converted rules */ - return new PropagateRuleCommand(vars, guards, heads, body, triggers); -} - -Command* PropagateRuleCommand::clone() const -{ - return new PropagateRuleCommand( - d_vars, d_guards, d_heads, d_body, d_triggers); -} - -std::string PropagateRuleCommand::getCommandName() const -{ - return "propagate-rule"; -} } // namespace CVC4 diff --git a/src/smt/command.h b/src/smt/command.h index d82399135..19b858bd6 100644 --- a/src/smt/command.h +++ b/src/smt/command.h @@ -1315,80 +1315,6 @@ class CVC4_PUBLIC DatatypeDeclarationCommand : public Command std::string getCommandName() const override; }; /* class DatatypeDeclarationCommand */ -class CVC4_PUBLIC RewriteRuleCommand : public Command -{ - public: - typedef std::vector > Triggers; - - protected: - typedef std::vector VExpr; - VExpr d_vars; - VExpr d_guards; - Expr d_head; - Expr d_body; - Triggers d_triggers; - - public: - RewriteRuleCommand(const std::vector& vars, - const std::vector& guards, - Expr head, - Expr body, - const Triggers& d_triggers); - RewriteRuleCommand(const std::vector& vars, Expr head, Expr body); - - const std::vector& getVars() const; - const std::vector& getGuards() const; - Expr getHead() const; - Expr getBody() const; - const Triggers& getTriggers() const; - - void invoke(SmtEngine* smtEngine) override; - Command* exportTo(ExprManager* exprManager, - ExprManagerMapCollection& variableMap) override; - Command* clone() const override; - std::string getCommandName() const override; -}; /* class RewriteRuleCommand */ - -class CVC4_PUBLIC PropagateRuleCommand : public Command -{ - public: - typedef std::vector > Triggers; - - protected: - typedef std::vector VExpr; - VExpr d_vars; - VExpr d_guards; - VExpr d_heads; - Expr d_body; - Triggers d_triggers; - bool d_deduction; - - public: - PropagateRuleCommand(const std::vector& vars, - const std::vector& guards, - const std::vector& heads, - Expr body, - const Triggers& d_triggers, - /* true if we want a deduction rule */ - bool d_deduction = false); - PropagateRuleCommand(const std::vector& vars, - const std::vector& heads, - Expr body, - bool d_deduction = false); - - const std::vector& getVars() const; - const std::vector& getGuards() const; - const std::vector& getHeads() const; - Expr getBody() const; - const Triggers& getTriggers() const; - bool isDeduction() const; - void invoke(SmtEngine* smtEngine) override; - Command* exportTo(ExprManager* exprManager, - ExprManagerMapCollection& variableMap) override; - Command* clone() const override; - std::string getCommandName() const override; -}; /* class PropagateRuleCommand */ - class CVC4_PUBLIC ResetCommand : public Command { public: diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index ad4d4e1d5..1d96fc207 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -3630,12 +3630,6 @@ void SmtEnginePrivate::addFormula( // n is the result of an unknown preprocessing step, add it to dependency map to null ProofManager::currentPM()->addDependence(n, Node::null()); } - // rewrite rules are by default in the unsat core because - // they need to be applied until saturation - if(options::unsatCores() && - n.getKind() == kind::REWRITE_RULE ){ - ProofManager::currentPM()->addUnsatCore(n.toExpr()); - } ); // Add the normalized formula to the queue diff --git a/src/theory/quantifiers/kinds b/src/theory/quantifiers/kinds index dc11ed562..1534d2d4d 100644 --- a/src/theory/quantifiers/kinds +++ b/src/theory/quantifiers/kinds @@ -55,25 +55,4 @@ typerule INST_ATTRIBUTE ::CVC4::theory::quantifiers::QuantifierInstAttributeType typerule INST_PATTERN_LIST ::CVC4::theory::quantifiers::QuantifierInstPatternListTypeRule typerule INST_CLOSURE ::CVC4::theory::quantifiers::QuantifierInstClosureTypeRule -# for rewrite rules -# types... -sort RRHB_TYPE \ - Cardinality::INTEGERS \ - not-well-founded \ - "head and body of the rule type (for rewrite-rules theory)" - -# operators... - -# variables, guards, RR_REWRITE/REDUCTION_RULE/DEDUCTION_RULE -operator REWRITE_RULE 3 "general rewrite rule (for rewrite-rules theory)" -#HEAD/BODY/TRIGGER -operator RR_REWRITE 2:3 "actual rewrite rule (for rewrite-rules theory)" -operator RR_REDUCTION 2:3 "actual reduction rule (for rewrite-rules theory)" -operator RR_DEDUCTION 2:3 "actual deduction rule (for rewrite-rules theory)" - -typerule REWRITE_RULE ::CVC4::theory::quantifiers::RewriteRuleTypeRule -typerule RR_REWRITE ::CVC4::theory::quantifiers::RRRewriteTypeRule -typerule RR_REDUCTION ::CVC4::theory::quantifiers::RRRedDedTypeRule -typerule RR_DEDUCTION ::CVC4::theory::quantifiers::RRRedDedTypeRule - endtheory diff --git a/src/theory/quantifiers/quantifiers_attributes.cpp b/src/theory/quantifiers/quantifiers_attributes.cpp index 0e6eb1581..af4011bd9 100644 --- a/src/theory/quantifiers/quantifiers_attributes.cpp +++ b/src/theory/quantifiers/quantifiers_attributes.cpp @@ -16,7 +16,6 @@ #include "options/quantifiers_options.h" #include "theory/arith/arith_msum.h" -#include "theory/quantifiers/rewrite_engine.h" #include "theory/quantifiers/sygus/synth_engine.h" #include "theory/quantifiers/term_util.h" #include "theory/quantifiers_engine.h" @@ -80,12 +79,6 @@ void QuantAttributes::setUserAttribute( const std::string& attr, Node n, std::ve Trace("quant-attr-debug") << "Set instantiation level " << n << " to " << lvl << std::endl; QuantInstLevelAttribute qila; n.setAttribute( qila, lvl ); - }else if( attr=="rr-priority" ){ - Assert(node_values.size() == 1); - uint64_t lvl = node_values[0].getConst().getNumerator().getLong(); - Trace("quant-attr-debug") << "Set rewrite rule priority " << n << " to " << lvl << std::endl; - RrPriorityAttribute rrpa; - n.setAttribute( rrpa, lvl ); }else if( attr=="quant-elim" ){ Trace("quant-attr-debug") << "Set quantifier elimination " << n << std::endl; QuantElimAttribute qea; @@ -97,21 +90,6 @@ void QuantAttributes::setUserAttribute( const std::string& attr, Node n, std::ve } } -bool QuantAttributes::checkRewriteRule( Node q ) { - return !getRewriteRule( q ).isNull(); -} - -Node QuantAttributes::getRewriteRule( Node q ) { - if (q.getKind() == FORALL && q.getNumChildren() == 3 - && q[2][0].getNumChildren() > 0 - && q[2][0][0].getKind() == REWRITE_RULE) - { - return q[2][0][0]; - }else{ - return Node::null(); - } -} - bool QuantAttributes::checkFunDef( Node q ) { return !getFunDefHead( q ).isNull(); } @@ -275,10 +253,6 @@ void QuantAttributes::computeQuantAttributes( Node q, QAttributes& qa ){ qa.d_qinstLevel = avar.getAttribute(QuantInstLevelAttribute()); Trace("quant-attr") << "Attribute : quant inst level " << qa.d_qinstLevel << " : " << q << std::endl; } - if( avar.hasAttribute(RrPriorityAttribute()) ){ - qa.d_rr_priority = avar.getAttribute(RrPriorityAttribute()); - Trace("quant-attr") << "Attribute : rr priority " << qa.d_rr_priority << " : " << q << std::endl; - } if( avar.getAttribute(QuantElimAttribute()) ){ Trace("quant-attr") << "Attribute : quantifier elimination : " << q << std::endl; qa.d_quant_elim = true; @@ -294,11 +268,6 @@ void QuantAttributes::computeQuantAttributes( Node q, QAttributes& qa ){ qa.d_qid_num = avar; Trace("quant-attr") << "Attribute : id number " << qa.d_qid_num.getAttribute(QuantIdNumAttribute()) << " : " << q << std::endl; } - if( avar.getKind()==REWRITE_RULE ){ - Trace("quant-attr") << "Attribute : rewrite rule : " << q << std::endl; - Assert(i == 0); - qa.d_rr = avar; - } } } } @@ -349,15 +318,6 @@ int QuantAttributes::getQuantInstLevel( Node q ) { } } -int QuantAttributes::getRewriteRulePriority( Node q ) { - std::map< Node, QAttributes >::iterator it = d_qattr.find( q ); - if( it==d_qattr.end() ){ - return -1; - }else{ - return it->second.d_rr_priority; - } -} - bool QuantAttributes::isQuantElim( Node q ) { std::map< Node, QAttributes >::iterator it = d_qattr.find( q ); if( it==d_qattr.end() ){ diff --git a/src/theory/quantifiers/quantifiers_attributes.h b/src/theory/quantifiers/quantifiers_attributes.h index 827c5e7f4..fc0f85956 100644 --- a/src/theory/quantifiers/quantifiers_attributes.h +++ b/src/theory/quantifiers/quantifiers_attributes.h @@ -111,7 +111,6 @@ struct QAttributes d_conjecture(false), d_axiom(false), d_sygus(false), - d_rr_priority(-1), d_qinstLevel(-1), d_quant_elim(false), d_quant_elim_partial(false) @@ -120,9 +119,6 @@ struct QAttributes ~QAttributes(){} /** does the quantified formula have a pattern? */ bool d_hasPattern; - /** if non-null, this is the rewrite rule representation of the quantified - * formula */ - Node d_rr; /** is this formula marked a conjecture? */ bool d_conjecture; /** is this formula marked an axiom? */ @@ -134,8 +130,6 @@ struct QAttributes bool d_sygus; /** side condition for sygus conjectures */ Node d_sygusSideCondition; - /** if a rewrite rule, then this is the priority value for the rewrite rule */ - int d_rr_priority; /** stores the maximum instantiation level allowed for this quantified formula * (-1 means allow any) */ int d_qinstLevel; @@ -150,8 +144,6 @@ struct QAttributes Node d_name; /** the quantifier id associated with this formula */ Node d_qid_num; - /** is this quantified formula a rewrite rule? */ - bool isRewriteRule() const { return !d_rr.isNull(); } /** is this quantified formula a function definition? */ bool isFunDef() const { return !d_fundef_f.isNull(); } /** @@ -193,10 +185,6 @@ public: /** compute the attributes for q */ void computeAttributes(Node q); - /** is quantifier treated as a rewrite rule? */ - static bool checkRewriteRule( Node q ); - /** get the rewrite rule associated with the quanfied formula */ - static Node getRewriteRule( Node q ); /** is fun def */ static bool checkFunDef( Node q ); /** is fun def */ diff --git a/src/theory/quantifiers/quantifiers_rewriter.cpp b/src/theory/quantifiers/quantifiers_rewriter.cpp index e35595287..e2ee99ceb 100644 --- a/src/theory/quantifiers/quantifiers_rewriter.cpp +++ b/src/theory/quantifiers/quantifiers_rewriter.cpp @@ -185,15 +185,13 @@ RewriteResponse QuantifiersRewriter::postRewrite(TNode in) { //compute attributes QAttributes qa; QuantAttributes::computeQuantAttributes( in, qa ); - if( !qa.isRewriteRule() ){ - for( int op=0; op vars; - vars.reserve(r[0].getNumChildren()); - for( Node::const_iterator v = r[0].begin(); v != r[0].end(); ++v ){ - vars.push_back(*v); - }; - - // Body/Remove_term/Guards/Triggers - Node body = r[2][1]; - TNode new_terms = r[2][1]; - std::vector guards; - std::vector pattern; - Node true_node = NodeManager::currentNM()->mkConst(true); - // shortcut - TNode head = r[2][0]; - switch(rrkind){ - case kind::RR_REWRITE: - // Equality - pattern.push_back( head ); - body = head.eqNode(body); - break; - case kind::RR_REDUCTION: - case kind::RR_DEDUCTION: - // Add head to guards and pattern - switch(head.getKind()){ - case kind::AND: - for( unsigned i = 0; i= 3 ){ - for( unsigned i=0; i forallB(kind::FORALL); - forallB << r[0]; - Node gg = guards.size()==0 ? true_node : ( guards.size()==1 ? guards[0] : NodeManager::currentNM()->mkNode( AND, guards ) ); - gg = NodeManager::currentNM()->mkNode( OR, gg.negate(), body ); - gg = Rewriter::rewrite( gg ); - forallB << gg; - NodeBuilder<> patternB(kind::INST_PATTERN); - patternB.append(pattern); - NodeBuilder<> patternListB(kind::INST_PATTERN_LIST); - //the entire rewrite rule is the first pattern - if( options::quantRewriteRules() ){ - patternListB << NodeManager::currentNM()->mkNode( INST_ATTRIBUTE, r ); - } - patternListB << static_cast(patternB); - forallB << static_cast(patternListB); - Node rn = (Node) forallB; - - return rn; -} - bool QuantifiersRewriter::isPrenexNormalForm( Node n ) { if( n.getKind()==FORALL ){ return n[1].getKind()!=FORALL && isPrenexNormalForm( n[1] ); @@ -2272,17 +2174,14 @@ Node QuantifiersRewriter::preSkolemizeQuantifiers( Node n, bool polarity, std::v Node QuantifiersRewriter::preprocess( Node n, bool isInst ) { Node prev = n; - if( n.getKind() == kind::REWRITE_RULE ){ - n = quantifiers::QuantifiersRewriter::rewriteRewriteRule( n ); - }else{ - if( options::preSkolemQuant() ){ - if( !isInst || !options::preSkolemQuantNested() ){ - Trace("quantifiers-preprocess-debug") << "Pre-skolemize " << n << "..." << std::endl; - //apply pre-skolemization to existential quantifiers - std::vector< TypeNode > fvTypes; - std::vector< TNode > fvs; - n = quantifiers::QuantifiersRewriter::preSkolemizeQuantifiers( prev, true, fvTypes, fvs ); - } + + if( options::preSkolemQuant() ){ + if( !isInst || !options::preSkolemQuantNested() ){ + Trace("quantifiers-preprocess-debug") << "Pre-skolemize " << n << "..." << std::endl; + //apply pre-skolemization to existential quantifiers + std::vector< TypeNode > fvTypes; + std::vector< TNode > fvs; + n = preSkolemizeQuantifiers( prev, true, fvTypes, fvs ); } } //pull all quantifiers globally @@ -2291,7 +2190,7 @@ Node QuantifiersRewriter::preprocess( Node n, bool isInst ) { { Trace("quantifiers-prenex") << "Prenexing : " << n << std::endl; std::map< unsigned, std::map< Node, Node > > visited; - n = quantifiers::QuantifiersRewriter::computePrenexAgg( n, true, visited ); + n = computePrenexAgg( n, true, visited ); n = Rewriter::rewrite( n ); Trace("quantifiers-prenex") << "Prenexing returned : " << n << std::endl; //Assert( isPrenexNormalForm( n ) ); diff --git a/src/theory/quantifiers/quantifiers_rewriter.h b/src/theory/quantifiers/quantifiers_rewriter.h index e8f069882..69e057c76 100644 --- a/src/theory/quantifiers/quantifiers_rewriter.h +++ b/src/theory/quantifiers/quantifiers_rewriter.h @@ -204,7 +204,6 @@ private: private: static Node preSkolemizeQuantifiers(Node n, bool polarity, std::vector< TypeNode >& fvTypes, std::vector& fvs); public: - static Node rewriteRewriteRule( Node r ); static bool isPrenexNormalForm( Node n ); /** preprocess * diff --git a/src/theory/quantifiers/rewrite_engine.cpp b/src/theory/quantifiers/rewrite_engine.cpp deleted file mode 100644 index 9903456c9..000000000 --- a/src/theory/quantifiers/rewrite_engine.cpp +++ /dev/null @@ -1,309 +0,0 @@ -/********************* */ -/*! \file rewrite_engine.cpp - ** \verbatim - ** Top contributors (to current version): - ** Andrew Reynolds, Tim King, Morgan Deters - ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS - ** in the top-level source directory) and their institutional affiliations. - ** All rights reserved. See the file COPYING in the top-level source - ** directory for licensing information.\endverbatim - ** - ** \brief Rewrite engine module - ** - ** This class manages rewrite rules for quantifiers - **/ - -#include "theory/quantifiers/rewrite_engine.h" - -#include "options/quantifiers_options.h" -#include "theory/quantifiers_engine.h" - -using namespace CVC4; -using namespace std; -using namespace CVC4::theory; -using namespace CVC4::theory::quantifiers; -using namespace CVC4::kind; - -struct PrioritySort { - std::vector< double > d_priority; - bool operator() (int i,int j) { - return d_priority[i] < d_priority[j]; - } -}; - -RewriteEngine::RewriteEngine(context::Context* c, - QuantifiersEngine* qe, - QuantConflictFind* qcf) - : QuantifiersModule(qe), d_qcf(qcf) -{ - d_needsSort = false; -} - -double RewriteEngine::getPriority( Node f ) { - Node rr = QuantAttributes::getRewriteRule( f ); - Node rrr = rr[2]; - Trace("rr-priority") << "Get priority : " << rrr << " " << rrr.getKind() << std::endl; - bool deterministic = rrr[1].getKind()!=OR; - - if( rrr.getKind()==RR_REWRITE ){ - return deterministic ? 0.0 : 3.0; - }else if( rrr.getKind()==RR_DEDUCTION ){ - return deterministic ? 1.0 : 4.0; - }else if( rrr.getKind()==RR_REDUCTION ){ - return deterministic ? 2.0 : 5.0; - }else{ - return 6.0; - } - - //return deterministic ? 0.0 : 1.0; -} - -bool RewriteEngine::needsCheck( Theory::Effort e ){ - return e==Theory::EFFORT_FULL; - //return e>=Theory::EFFORT_LAST_CALL; -} - -void RewriteEngine::check(Theory::Effort e, QEffort quant_e) -{ - if (quant_e == QEFFORT_STANDARD) - { - Assert(!d_quantEngine->inConflict()); - Trace("rewrite-engine") << "---Rewrite Engine Round, effort = " << e << "---" << std::endl; - //if( e==Theory::EFFORT_LAST_CALL ){ - // if( !d_quantEngine->getModel()->isModelSet() ){ - // d_quantEngine->getTheoryEngine()->getModelBuilder()->buildModel( d_quantEngine->getModel(), true ); - // } - //} - if( d_needsSort ){ - d_priority_order.clear(); - PrioritySort ps; - std::vector< int > indicies; - for( int i=0; i<(int)d_rr_quant.size(); i++ ){ - ps.d_priority.push_back( getPriority( d_rr_quant[i] ) ); - indicies.push_back( i ); - } - std::sort( indicies.begin(), indicies.end(), ps ); - for( unsigned i=0; iinConflict() && success && index<(int)d_priority_order.size() ) { - addedLemmas += checkRewriteRule( d_priority_order[index], e ); - index++; - if( index<(int)d_priority_order.size() ){ - success = addedLemmas==0 || getPriority( d_priority_order[index] )==getPriority( d_priority_order[index-1] ); - } - } - - Trace("rewrite-engine") << "Finished rewrite engine, added " << addedLemmas << " lemmas." << std::endl; - } -} - -int RewriteEngine::checkRewriteRule( Node f, Theory::Effort e ) { - Trace("rewrite-engine-inst") << "Check " << d_qinfo_n[f] << ", priority = " << getPriority( f ) << ", effort = " << e << "..." << std::endl; - - // get the proper quantifiers info - std::map::iterator it = d_qinfo.find(f); - if (it == d_qinfo.end()) - { - Trace("rewrite-engine-inst-debug") << "...No qinfo." << std::endl; - return 0; - } - // reset QCF module - QuantInfo* qi = &it->second; - if (!qi->matchGeneratorIsValid()) - { - Trace("rewrite-engine-inst-debug") << "...Invalid qinfo." << std::endl; - return 0; - } - d_qcf->setEffort(QuantConflictFind::EFFORT_CONFLICT); - Node rr = QuantAttributes::getRewriteRule(f); - Trace("rewrite-engine-inst-debug") << " Reset round..." << std::endl; - qi->reset_round(d_qcf); - Trace("rewrite-engine-inst-debug") << " Get matches..." << std::endl; - int addedLemmas = 0; - while (!d_quantEngine->inConflict() && qi->getNextMatch(d_qcf) - && (addedLemmas == 0 || !options::rrOneInstPerRound())) - { - Trace("rewrite-engine-inst-debug") - << " Got match to complete..." << std::endl; - qi->debugPrintMatch("rewrite-engine-inst-debug"); - std::vector assigned; - if (!qi->isMatchSpurious(d_qcf)) - { - bool doContinue = false; - bool success = true; - int tempAddedLemmas = 0; - while (!d_quantEngine->inConflict() && tempAddedLemmas == 0 && success - && (addedLemmas == 0 || !options::rrOneInstPerRound())) - { - success = qi->completeMatch(d_qcf, assigned, doContinue); - doContinue = true; - if (success) - { - Trace("rewrite-engine-inst-debug") - << " Construct match..." << std::endl; - std::vector inst; - qi->getMatch(inst); - if (Trace.isOn("rewrite-engine-inst-debug")) - { - Trace("rewrite-engine-inst-debug") - << " Add instantiation..." << std::endl; - for (unsigned i = 0, nchild = f[0].getNumChildren(); i < nchild; - i++) - { - Trace("rewrite-engine-inst-debug") << " " << f[0][i] << " -> "; - if (i < inst.size()) - { - Trace("rewrite-engine-inst-debug") << inst[i] << std::endl; - } - else - { - Trace("rewrite-engine-inst-debug") - << "OUT_OF_RANGE" << std::endl; - Assert(false); - } - } - } - // resize to remove auxiliary variables - if (inst.size() > f[0].getNumChildren()) - { - inst.resize(f[0].getNumChildren()); - } - if (d_quantEngine->getInstantiate()->addInstantiation(f, inst)) - { - addedLemmas++; - tempAddedLemmas++; - } - else - { - Trace("rewrite-engine-inst-debug") << " - failed." << std::endl; - } - Trace("rewrite-engine-inst-debug") - << " Get next completion..." << std::endl; - } - } - Trace("rewrite-engine-inst-debug") - << " - failed to complete." << std::endl; - } - else - { - Trace("rewrite-engine-inst-debug") - << " - match is spurious." << std::endl; - } - Trace("rewrite-engine-inst-debug") << " Get next match..." << std::endl; - } - d_quantEngine->d_statistics.d_instantiations_rr += addedLemmas; - Trace("rewrite-engine-inst") << "-> Generated " << addedLemmas << " lemmas." << std::endl; - return addedLemmas; -} - -void RewriteEngine::registerQuantifier( Node f ) { - Node rr = QuantAttributes::getRewriteRule( f ); - if (rr.isNull()) - { - return; - } - Trace("rr-register") << "Register quantifier " << f << std::endl; - Trace("rr-register") << " rewrite rule is : " << rr << std::endl; - d_rr_quant.push_back(f); - d_rr[f] = rr; - d_needsSort = true; - Trace("rr-register") << " guard is : " << d_rr[f][1] << std::endl; - - std::vector qcfn_c; - - std::vector bvl; - bvl.insert(bvl.end(), f[0].begin(), f[0].end()); - - NodeManager* nm = NodeManager::currentNM(); - std::vector cc; - // add patterns - for (unsigned i = 1, nchild = f[2].getNumChildren(); i < nchild; i++) - { - std::vector nc; - for (const Node& pat : f[2][i]) - { - Node nn; - Node nbv = nm->mkBoundVar(pat.getType()); - if (pat.getType().isBoolean() && pat.getKind() != APPLY_UF) - { - nn = pat.negate(); - } - else - { - nn = pat.eqNode(nbv).negate(); - bvl.push_back(nbv); - } - nc.push_back(nn); - } - if (!nc.empty()) - { - Node n = nc.size() == 1 ? nc[0] : nm->mkNode(AND, nc); - Trace("rr-register-debug") << " pattern is " << n << std::endl; - if (std::find(cc.begin(), cc.end(), n) == cc.end()) - { - cc.push_back(n); - } - } - } - qcfn_c.push_back(nm->mkNode(BOUND_VAR_LIST, bvl)); - - std::vector body_c; - // add the guards - if (d_rr[f][1].getKind() == AND) - { - for (const Node& g : d_rr[f][1]) - { - if (MatchGen::isHandled(g)) - { - body_c.push_back(g.negate()); - } - } - } - else if (d_rr[f][1] != d_quantEngine->getTermUtil()->d_true) - { - if (MatchGen::isHandled(d_rr[f][1])) - { - body_c.push_back(d_rr[f][1].negate()); - } - } - // add the patterns to the body - body_c.push_back(cc.size() == 1 ? cc[0] : nm->mkNode(AND, cc)); - // make the body - qcfn_c.push_back(body_c.size() == 1 ? body_c[0] : nm->mkNode(OR, body_c)); - // make the quantified formula - d_qinfo_n[f] = nm->mkNode(FORALL, qcfn_c); - Trace("rr-register") << " qcf formula is : " << d_qinfo_n[f] << std::endl; - d_qinfo[f].initialize(d_qcf, d_qinfo_n[f], d_qinfo_n[f][1]); -} - -void RewriteEngine::assertNode( Node n ) { - -} - -bool RewriteEngine::checkCompleteFor( Node q ) { - // by semantics of rewrite rules, saturation -> SAT - return std::find( d_rr_quant.begin(), d_rr_quant.end(), q )!=d_rr_quant.end(); -} - -Node RewriteEngine::getInstConstNode( Node n, Node q ) { - std::map< Node, Node >::iterator it = d_inst_const_node[q].find( n ); - if( it==d_inst_const_node[q].end() ){ - Node nn = - d_quantEngine->getTermUtil()->substituteBoundVariablesToInstConstants( - n, q); - d_inst_const_node[q][n] = nn; - return nn; - }else{ - return it->second; - } -} diff --git a/src/theory/quantifiers/rewrite_engine.h b/src/theory/quantifiers/rewrite_engine.h deleted file mode 100644 index 29aba0f1a..000000000 --- a/src/theory/quantifiers/rewrite_engine.h +++ /dev/null @@ -1,86 +0,0 @@ -/********************* */ -/*! \file rewrite_engine.h - ** \verbatim - ** Top contributors (to current version): - ** Andrew Reynolds, Mathias Preiner - ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS - ** in the top-level source directory) and their institutional affiliations. - ** All rights reserved. See the file COPYING in the top-level source - ** directory for licensing information.\endverbatim - ** - ** [[ Add lengthier description here ]] - ** \todo document this file -**/ - -#include "cvc4_private.h" - -#ifndef CVC4__REWRITE_ENGINE_H -#define CVC4__REWRITE_ENGINE_H - -#include -#include - -#include "expr/attribute.h" -#include "theory/quantifiers/ematching/trigger.h" -#include "theory/quantifiers/quant_conflict_find.h" -#include "theory/quantifiers/quant_util.h" - -namespace CVC4 { -namespace theory { - -/** - * An attribute for marking a priority value for rewrite rules. - */ -struct RrPriorityAttributeId -{ -}; -typedef expr::Attribute RrPriorityAttribute; - -namespace quantifiers { - -class RewriteEngine : public QuantifiersModule -{ - std::vector< Node > d_rr_quant; - std::vector< Node > d_priority_order; - std::map< Node, Node > d_rr; - /** explicitly provided patterns */ - std::map< Node, std::vector< inst::Trigger* > > d_rr_triggers; - /** get the quantifer info object */ - std::map< Node, Node > d_qinfo_n; - std::map< Node, QuantInfo > d_qinfo; - double getPriority( Node f ); - bool d_needsSort; - std::map< Node, std::map< Node, Node > > d_inst_const_node; - Node getInstConstNode( Node n, Node q ); - - private: - int checkRewriteRule( Node f, Theory::Effort e ); - - public: - RewriteEngine(context::Context* c, - QuantifiersEngine* qe, - QuantConflictFind* qcf); - - bool needsCheck(Theory::Effort e) override; - void check(Theory::Effort e, QEffort quant_e) override; - void registerQuantifier(Node f) override; - void assertNode(Node n) override; - bool checkCompleteFor(Node q) override; - /** Identify this module */ - std::string identify() const override { return "RewriteEngine"; } - - private: - /** - * A pointer to the quantifiers conflict find module of the quantifiers - * engine. This is the module that computes instantiations for rewrite rule - * quantifiers. - */ - QuantConflictFind* d_qcf; -}; - -} -} -} - -#endif diff --git a/src/theory/quantifiers/theory_quantifiers_type_rules.h b/src/theory/quantifiers/theory_quantifiers_type_rules.h index a83dbf541..e2c9043a1 100644 --- a/src/theory/quantifiers/theory_quantifiers_type_rules.h +++ b/src/theory/quantifiers/theory_quantifiers_type_rules.h @@ -141,91 +141,6 @@ struct QuantifierInstClosureTypeRule { } };/* struct QuantifierInstClosureTypeRule */ - -class RewriteRuleTypeRule { -public: - - /** - * Compute the type for (and optionally typecheck) a term belonging - * to the theory of rewriterules. - * - * @param nodeManager the NodeManager in use - * @param n the node to compute the type of - * @param check if true, the node's type should be checked as well - * as computed. - */ - inline static TypeNode computeType(NodeManager* nodeManager, TNode n, - bool check) - { - Debug("typecheck-r") << "type check for rr " << n << std::endl; - Assert(n.getKind() == kind::REWRITE_RULE && n.getNumChildren() == 3); - if( check ){ - if( n[ 0 ].getType(check)!=nodeManager->boundVarListType() ){ - throw TypeCheckingExceptionPrivate(n[0], - "first argument of rewrite rule is not bound var list"); - } - if( n[ 1 ].getType(check)!=nodeManager->booleanType() ){ - throw TypeCheckingExceptionPrivate(n[1], - "guard of rewrite rule is not an actual guard"); - } - if( n[2].getType(check) != - TypeNode(nodeManager->mkTypeConst(RRHB_TYPE))){ - throw TypeCheckingExceptionPrivate(n[2], - "not a correct rewrite rule"); - } - } - return nodeManager->booleanType(); - } -};/* class RewriteRuleTypeRule */ - -class RRRewriteTypeRule { -public: - - inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check) - { - Assert(n.getKind() == kind::RR_REWRITE); - if( check ){ - if( n[0].getType(check)!=n[1].getType(check) ){ - throw TypeCheckingExceptionPrivate(n, - "terms of rewrite rule are not equal"); - } - if( n.getNumChildren() == 3 && n[2].getType(check)!=nodeManager->instPatternListType() ){ - throw TypeCheckingExceptionPrivate(n, "third argument of rewrite rule is not instantiation pattern list"); - } - if( n[0].getKind()!=kind::APPLY_UF ){ - throw TypeCheckingExceptionPrivate(n[0], "head of rewrite rules must start with an uninterpreted symbols. If you want to write a propagation rule, add the guard [true] for disambiguation"); - } - } - return TypeNode(nodeManager->mkTypeConst(RRHB_TYPE)); - } -};/* struct QuantifierReductionRuleRule */ - -class RRRedDedTypeRule { -public: - - inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check) - { - Assert(n.getKind() == kind::RR_REDUCTION - || n.getKind() == kind::RR_DEDUCTION); - if( check ){ - if( n[ 0 ].getType(check)!=nodeManager->booleanType() ){ - throw TypeCheckingExceptionPrivate(n, "head of reduction rule is not boolean"); - } - if( n[ 1 ].getType(check)!=nodeManager->booleanType() ){ - throw TypeCheckingExceptionPrivate(n, "body of reduction rule is not boolean"); - } - if( n.getNumChildren() == 3 && n[2].getType(check)!=nodeManager->instPatternListType() ){ - throw TypeCheckingExceptionPrivate(n, "third argument of rewrite rule is not instantiation pattern list"); - } - if( n.getNumChildren() < 3 && n[ 0 ] == nodeManager->mkConst(true) ){ - throw TypeCheckingExceptionPrivate(n, "A rewrite rule must have one head or one trigger at least"); - } - } - return TypeNode(nodeManager->mkTypeConst(RRHB_TYPE)); - } -};/* struct QuantifierReductionRuleRule */ - - }/* CVC4::theory::quantifiers namespace */ }/* CVC4::theory namespace */ }/* CVC4 namespace */ diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp index c7eafc3b8..80a493496 100644 --- a/src/theory/quantifiers_engine.cpp +++ b/src/theory/quantifiers_engine.cpp @@ -30,7 +30,6 @@ #include "theory/quantifiers/quant_conflict_find.h" #include "theory/quantifiers/quant_split.h" #include "theory/quantifiers/quantifiers_rewriter.h" -#include "theory/quantifiers/rewrite_engine.h" #include "theory/quantifiers/sygus/synth_engine.h" #include "theory/sep/theory_sep.h" #include "theory/theory_engine.h" @@ -53,7 +52,6 @@ class QuantifiersEnginePrivate d_model_engine(nullptr), d_bint(nullptr), d_qcf(nullptr), - d_rr_engine(nullptr), d_sg_gen(nullptr), d_synth_e(nullptr), d_lte_part_inst(nullptr), @@ -81,8 +79,6 @@ class QuantifiersEnginePrivate std::unique_ptr d_bint; /** Conflict find mechanism for quantifiers */ std::unique_ptr d_qcf; - /** rewrite rules utility */ - std::unique_ptr d_rr_engine; /** subgoal generator */ std::unique_ptr d_sg_gen; /** ceg instantiation */ @@ -111,7 +107,7 @@ class QuantifiersEnginePrivate bool& needsBuilder) { // add quantifiers modules - if (options::quantConflictFind() || options::quantRewriteRules()) + if (options::quantConflictFind()) { d_qcf.reset(new quantifiers::QuantConflictFind(qe, c)); modules.push_back(d_qcf.get()); @@ -150,11 +146,6 @@ class QuantifiersEnginePrivate // finite model finder has special ways of building the model needsBuilder = true; } - if (options::quantRewriteRules()) - { - d_rr_engine.reset(new quantifiers::RewriteEngine(c, qe, d_qcf.get())); - modules.push_back(d_rr_engine.get()); - } if (options::ltePartialInst()) { d_lte_part_inst.reset(new quantifiers::LtePartialInst(qe, c)); @@ -397,16 +388,6 @@ void QuantifiersEngine::setOwner( Node q, QuantifiersModule * m, int priority ) void QuantifiersEngine::setOwner(Node q, quantifiers::QAttributes& qa) { - if (!qa.d_rr.isNull()) - { - if (d_private->d_rr_engine.get() == nullptr) - { - Trace("quant-warn") << "WARNING : rewrite engine is null, and we have : " - << q << std::endl; - } - // set rewrite engine as owner - setOwner(q, d_private->d_rr_engine.get(), 2); - } if (qa.d_sygus || (options::sygusRecFun() && !qa.d_fundef_f.isNull())) { if (d_private->d_synth_e.get() == nullptr) diff --git a/src/theory/term_registration_visitor.cpp b/src/theory/term_registration_visitor.cpp index 3b11d8e54..6a404104f 100644 --- a/src/theory/term_registration_visitor.cpp +++ b/src/theory/term_registration_visitor.cpp @@ -35,7 +35,7 @@ bool PreRegisterVisitor::alreadyVisited(TNode current, TNode parent) { Debug("register::internal") << "PreRegisterVisitor::alreadyVisited(" << current << "," << parent << ")" << std::endl; - if ((parent.isClosure() || parent.getKind() == kind::REWRITE_RULE + if ((parent.isClosure() || parent.getKind() == kind::SEP_STAR || parent.getKind() == kind::SEP_WAND || (parent.getKind() == kind::SEP_LABEL && current.getType().isBoolean()) @@ -178,7 +178,7 @@ bool SharedTermsVisitor::alreadyVisited(TNode current, TNode parent) const { Debug("register::internal") << "SharedTermsVisitor::alreadyVisited(" << current << "," << parent << ")" << std::endl; - if ((parent.isClosure() || parent.getKind() == kind::REWRITE_RULE + if ((parent.isClosure() || parent.getKind() == kind::SEP_STAR || parent.getKind() == kind::SEP_WAND || (parent.getKind() == kind::SEP_LABEL && current.getType().isBoolean()) diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt index 150983187..ca50e2c83 100644 --- a/test/regress/CMakeLists.txt +++ b/test/regress/CMakeLists.txt @@ -797,11 +797,6 @@ set(regress_0_tests regress0/rels/relations-ops.smt2 regress0/rels/rels-sharing-simp.cvc regress0/reset-assertions.smt2 - regress0/rewriterules/datatypes.smt2 - regress0/rewriterules/length_trick.smt2 - regress0/rewriterules/native_arrays.smt2 - regress0/rewriterules/relation.smt2 - regress0/rewriterules/simulate_rewriting.smt2 regress0/sep/dispose-1.smt2 regress0/sep/dup-nemp.smt2 regress0/sep/nemp.smt2 @@ -1344,7 +1339,6 @@ set(regress_1_tests regress1/push-pop/arith_lra_02.smt2 regress1/push-pop/bug-fmf-fun-skolem.smt2 regress1/push-pop/bug216.smt2 - regress1/push-pop/bug326.smt2 regress1/push-pop/fuzz_1.smt2 regress1/push-pop/fuzz_10.smt2 regress1/push-pop/fuzz_11.smt2 @@ -1542,15 +1536,6 @@ set(regress_1_tests regress1/rels/rel_tp_join_2_1.cvc regress1/rels/set-strat.cvc regress1/rels/strat.cvc - regress1/rewriterules/datatypes_sat.smt2 - regress1/rewriterules/length_gen.smt2 - regress1/rewriterules/length_gen_020.smt2 - regress1/rewriterules/length_gen_020_sat.smt2 - regress1/rewriterules/length_gen_040.smt2 - regress1/rewriterules/length_gen_040_lemma.smt2 - regress1/rewriterules/length_gen_040_lemma_trigger.smt2 - regress1/rewriterules/reachability_back_to_the_future.smt2 - regress1/rewriterules/read5.smt2 regress1/rr-verify/bool-crci.sy regress1/rr-verify/bv-term-32.sy regress1/rr-verify/bv-term.sy @@ -2179,12 +2164,6 @@ set(regression_disabled_tests regress0/quantifiers/qbv-test-invert-bvshl-0-neq.smt2 regress0/quantifiers/qbv-test-invert-concat-0-neq.smt2 regress0/quantifiers/qbv-test-invert-concat-1-neq.smt2 - regress0/rewriterules/datatypes_clark.smt2 - regress0/rewriterules/length.smt2 - regress0/rewriterules/length_gen_n.smt2 - regress0/rewriterules/length_gen_n_lemma.smt2 - regress0/rewriterules/length_trick2.smt2 - regress0/rewriterules/native_datatypes.smt2 regress0/sets/mar2014/stacks0.hs.78.cvc4.smt2 regress0/sets/setel-eq.smt2 regress0/sets/sets-new.smt2 @@ -2322,20 +2301,6 @@ set(regression_disabled_tests # doing a coverage build with LFSC. regress1/quantifiers/set3.smt2 regress1/rels/garbage_collect.cvc - regress1/rewriterules/datatypes2.smt2 - regress1/rewriterules/datatypes3.smt2 - regress1/rewriterules/datatypes_clark_quantification.smt2 - regress1/rewriterules/length_gen_010.smt2 - regress1/rewriterules/length_gen_010_lemma.smt2 - regress1/rewriterules/length_gen_080.smt2 - regress1/rewriterules/length_gen_160_lemma.smt2 - regress1/rewriterules/length_gen_inv_160.smt2 - regress1/rewriterules/length_trick3.smt2 - regress1/rewriterules/length_trick3_int.smt2 - regress1/rewriterules/set_A_new_fast_tableau-base.smt2 - regress1/rewriterules/set_A_new_fast_tableau-base_sat.smt2 - regress1/rewriterules/test_guards.smt2 - regress1/rewriterules/why3_vstte10_max_sum_harness2.smt2 regress1/sets/setofsets-disequal.smt2 regress1/sets/finite-type/sets-card-neg-mem-union-2.smt2 regress1/simple-rdl-definefun.smt2 diff --git a/test/regress/regress0/rewriterules/datatypes.smt2 b/test/regress/regress0/rewriterules/datatypes.smt2 deleted file mode 100644 index 9a5f68100..000000000 --- a/test/regress/regress0/rewriterules/datatypes.smt2 +++ /dev/null @@ -1,102 +0,0 @@ -; COMMAND-LINE: --rewrite-rules -;; try to solve datatypes with rewriterules -(set-logic AUFLIA) -(set-info :status unsat) - -;; lists 2 nil -(declare-sort elt 0) ;; we suppose that elt is infinite -(declare-sort list 0) - -(declare-fun nil1 () list) -(declare-fun nil2 () list) -(declare-fun cons (elt list) list) - -;;;;;;;;;;;;;;;;;;;; -;; injective - -(declare-fun inj1 (list) elt) -(assert (forall ((?e elt) (?l list)) - (! (! (=> true (=> true (= (inj1 (cons ?e ?l)) ?e))) :pattern ((cons ?e ?l)) ) :rewrite-rule) )) - -(declare-fun inj2 (list) list) -(assert (forall ((?e elt) (?l list)) - (! (! (=> true (=> true (= (inj2 (cons ?e ?l)) ?l))) :pattern ((cons ?e ?l)) ) :rewrite-rule) )) - -;;;;;;;;;;;;;;;;;;;; -;; projection - -(declare-fun proj1 (list) elt) -(assert (forall ((?e elt) (?l list)) - (! (= (proj1 (cons ?e ?l)) ?e) :rewrite-rule) )) - -(declare-fun proj2 (list) list) -(assert (forall ((?e elt) (?l list)) - (! (= (proj2 (cons ?e ?l)) ?l) :rewrite-rule) )) - -;;;;;;;;;;;;;;;;;;; -;; test -(declare-fun iscons (list) Bool) -(assert (= (iscons nil1) false)) -(assert (= (iscons nil2) false)) -(assert (forall ((?e elt) (?l list)) - (! (! (=> true (=> true (= (iscons (cons ?e ?l)) true))) :pattern ((cons ?e ?l)) ) :rewrite-rule) )) - -(assert (forall ((?l list)) - (! (! (=> true (=> (iscons ?l) (= ?l (cons (proj1 ?l) (proj2 ?l))))) :pattern ((proj1 ?l)) ) :rewrite-rule) )) -(assert (forall ((?l list)) - (! (! (=> true (=> (iscons ?l) (= ?l (cons (proj1 ?l) (proj2 ?l))))) :pattern ((proj2 ?l)) ) :rewrite-rule) )) - - -(declare-fun isnil1 (list) Bool) -(assert (= (isnil1 nil1) true)) -(assert (= (isnil1 nil2) false)) -(assert (forall ((?e elt) (?l list)) - (! (= (isnil1 (cons ?e ?l)) false) :rewrite-rule) )) -(assert (forall ((?l list)) - (! (=> true (=> (isnil1 ?l) (= ?l nil1))) :rewrite-rule) )) - -(declare-fun isnil2 (list) Bool) -(assert (= (isnil2 nil1) false)) -(assert (= (isnil2 nil2) true)) -(assert (forall ((?e elt) (?l list)) - (! (= (isnil2 (cons ?e ?l)) false) :rewrite-rule) )) -(assert (forall ((?l list)) - (! (=> true (=> (isnil2 ?l) (= ?l nil2))) :rewrite-rule) )) - -;; distinct -(assert (forall ((?l list)) - (! (=> (isnil1 ?l) (and (not (isnil2 ?l)) (not (iscons ?l))) ) :rewrite-rule) )) - -(assert (forall ((?l list)) - (! (=> (isnil2 ?l) (and (not (isnil1 ?l)) (not (iscons ?l))) ) :rewrite-rule) )) - -(assert (forall ((?l list)) - (! (=> (iscons ?l) (and (not (isnil1 ?l)) (not (isnil2 ?l))) ) :rewrite-rule) )) - - -;;;;;;;;;;;;;;;;;;; -;; case-split -(assert (forall ((?l list)) - (! (! (=> true (or (isnil1 ?l) (isnil2 ?l) (iscons ?l))) :pattern ((proj1 ?l)) ) :rewrite-rule) )) -(assert (forall ((?l list)) - (! (! (=> true (or (isnil1 ?l) (isnil2 ?l) (iscons ?l))) :pattern ((proj2 ?l)) ) :rewrite-rule) )) - -;;;;;;;;;;;;;;;;;;; -;; finite case-split -(assert (forall ((?l list)) - (! (=> (not (iscons ?l)) (or (isnil1 ?l) (isnil2 ?l))) :rewrite-rule) )) - - - -;;;;; goal - -(declare-fun e () elt) -(declare-fun l1 () list) -(declare-fun l2 () list) - - -(assert (not (=> (iscons l1) (=> (= (proj2 l1) (proj2 l2)) (= l1 (cons (proj1 l1) (proj2 l2))))))) - -(check-sat) - -(exit) diff --git a/test/regress/regress0/rewriterules/datatypes_clark.smt2 b/test/regress/regress0/rewriterules/datatypes_clark.smt2 deleted file mode 100644 index cc217fc79..000000000 --- a/test/regress/regress0/rewriterules/datatypes_clark.smt2 +++ /dev/null @@ -1,205 +0,0 @@ -; COMMAND-LINE: --rewrite-rules -(set-logic AUFLIRA) - -;; DATATYPE -;; nat = succ(pred : nat) | zero, -;; list = cons(car : tree, cdr : list) | null, -;; tree = node(children : list) | leaf(data : nat) -;; END; - -;;;;;;;;;;; -;; nat ;; -;;;;;;;;;;; -(declare-sort nat 0) -(declare-fun zero () nat) -(declare-fun succ (nat) nat) - -;;;;;;;;;;;;;;;; -;; injective - -(declare-fun inj1 (nat) nat) -(assert-propagation((?x1 nat)) - (((succ ?x1))) () () (= (inj1 (succ ?x1)) ?x1) ) - -;;;;;;;;;;;;;;;;;;;; -;; projection - -(declare-fun pred (nat) nat) -(assert-rewrite ((?x1 nat)) () () (pred (succ ?x1)) ?x1 ) - -(assert (= (pred zero) zero)) - -;;;;;;;;;;;;;;;;;;; -;; test -(declare-fun is_succ (nat) Bool) -(assert (= (is_succ zero) false)) -(assert-propagation ((?x1 nat)) (((succ ?x1))) () () (= (is_succ (succ ?x1)) true) ) - -(assert-propagation ((?x1 nat)) (((pred ?x1))) () ((is_succ ?x1)) (= ?x1 (succ (pred ?x1)))) - -(declare-fun is_zero (nat) Bool) -(assert (= (is_zero zero) true)) -(assert-propagation ((?x1 nat)) () () ((is_zero ?x1)) (= ?x1 zero)) - -;;; directrr -(assert-rewrite ((?x1 nat)) () () (is_succ (succ ?x1)) true ) -(assert-rewrite ((?x1 nat)) () () (is_zero (succ ?x1)) false ) - - -;;;;;;;;;;;;;;;;;;;; -;; distinct -(assert-propagation ((?x1 nat)) () () ((is_zero ?x1)) (not (is_succ ?x1)) ) -(assert-propagation ((?x1 nat)) () () ((is_succ ?x1)) (not (is_zero ?x1)) ) -(assert-propagation ((?x1 nat)) () () ((not (is_zero ?x1))) (is_succ ?x1) ) -(assert-propagation ((?x1 nat)) () () ((not (is_succ ?x1))) (is_zero ?x1) ) - -;;;;;;;;;;;;;;;;;;; -;; case-split -(assert-propagation ((?x1 nat)) (((pred ?x1))) () () (or (is_zero ?x1) (is_succ ?x1)) ) - -;;;;;;;;;;;;;;;;;;; -;; non-cyclic -(declare-fun size_nat (nat) Real) -(assert-propagation ((?x1 nat)) (((succ ?x1))) () () (> (size_nat (succ ?x1)) (size_nat ?x1)) ) - - - -;;;;;;;;;;;;;;;;;;;;; -;; list and tree - -(declare-sort list 0) -(declare-sort tree 0) - -;;;;;;;;;;; -;; list ;; -;;;;;;;;;;; - -(declare-fun null () list) -(declare-fun cons (tree list) list) - -(declare-fun node (list) tree) -(declare-fun leaf (nat) tree) - -;;;;;;;;;;;;;;;; -;; injective - -(declare-fun inj2 (list) tree) -(assert-propagation ((?x1 tree) (?x2 list)) (((cons ?x1 ?x2))) () () (= (inj2 (cons ?x1 ?x2)) ?x1) ) - -(declare-fun inj3 (list) list) -(assert-propagation ((?x1 tree) (?x2 list)) (((cons ?x1 ?x2))) () () (= (inj3 (cons ?x1 ?x2)) ?x2) ) - - -;;;;;;;;;;;;;;;;;;;; -;; projection - -(declare-fun car (list) tree) -(assert-rewrite ((?x1 tree) (?x2 list)) () () (car (cons ?x1 ?x2)) ?x1) - -(assert (= (car null) (node null))) - -(declare-fun cdr (list) list) -(assert-rewrite ((?x1 tree) (?x2 list)) () () (cdr (cons ?x1 ?x2)) ?x2) - -(assert (= (cdr null) null)) - -;;;;;;;;;;;;;;;;;;; -;; test -(declare-fun is_cons (list) Bool) -(assert (= (is_cons null) false)) -(assert-propagation ((?x1 tree) (?x2 list)) (((cons ?x1 ?x2))) () () (= (is_cons (cons ?x1 ?x2)) true) ) - -(assert-propagation ((?x1 list)) (((car ?x1))) () ((is_cons ?x1)) (= ?x1 (cons (car ?x1) (cdr ?x1))) ) -(assert-propagation ((?x1 list)) (((cdr ?x1))) () ((is_cons ?x1)) (= ?x1 (cons (car ?x1) (cdr ?x1))) ) - -(declare-fun is_null (list) Bool) -(assert (= (is_null null) true)) - -(assert-propagation ((?x1 list)) (((car ?x1))) () ((is_null ?x1)) (= (car ?x1) (node null)) ) -(assert-propagation ((?x1 list)) (((cdr ?x1))) () ((is_null ?x1)) (= (cdr ?x1) null) ) - -(assert-propagation ((?x1 list)) () () ((is_null ?x1)) (= ?x1 null)) - -;;; directrr -(assert-rewrite ((?x1 tree) (?x2 list)) () () (is_cons (cons ?x1 ?x2)) true) -(assert-rewrite ((?x1 tree) (?x2 list)) () () (is_null (cons ?x1 ?x2)) false) - - - -;;;;;;;;;;;;;;;;;;;; -;; distinct -(assert-propagation ((?x1 list)) () () ((is_null ?x1)) (not (is_cons ?x1)) ) -(assert-propagation ((?x1 list)) () () ((is_cons ?x1)) (not (is_null ?x1)) ) -(assert-propagation ((?x1 list)) () () ((not (is_null ?x1))) (is_cons ?x1) ) -(assert-propagation ((?x1 list)) () () ((not (is_cons ?x1))) (is_null ?x1) ) - -;;;;;;;;;;;;;;;;;;; -;; case-split -(assert-propagation ((?x1 list)) (((car ?x1))) () () (or (is_null ?x1) (is_cons ?x1)) ) -(assert-propagation ((?x1 list)) (((cdr ?x1))) () () (or (is_null ?x1) (is_cons ?x1)) ) - -;;;;;;;;;;;;;;; -;; tree - -;;;;;;;;;;;;;;;; -;; injective - -(declare-fun inj4 (tree) list) -(assert-propagation ((?x1 list)) (((node ?x1))) () () (= (inj4 (node ?x1)) ?x1) ) - -(declare-fun inj5 (tree) nat) -(assert-propagation ((?x1 nat)) (((leaf ?x1))) () () (= (inj5 (leaf ?x1)) ?x1) ) - - -;;;;;;;;;;;;;;;;;;;; -;; projection - -(declare-fun children (tree) list) -(assert-rewrite ((?x1 list)) () () (children (node ?x1)) ?x1 ) -(assert-rewrite ((?x1 nat)) () () (children (leaf ?x1)) null ) - -(declare-fun data (tree) nat) -(assert-rewrite ((?x1 nat)) () () (data (leaf ?x1)) ?x1 ) -(assert-rewrite ((?x1 list)) () () (data (node ?x1)) zero ) - -;;;;;;;;;;;;;;;;;;; -;; test -(declare-fun is_node (tree) Bool) -(assert-propagation ((?x1 list)) (((node ?x1))) () () (= (is_node (node ?x1)) true) ) - -(assert-propagation ((?x1 tree)) (((children ?x1))) () ((is_node ?x1)) (= ?x1 (node (children ?x1))) ) -(assert-propagation ((?x1 tree)) (((data ?x1))) () ((is_node ?x1)) (= (data ?x1) zero) ) - - -(declare-fun is_leaf (tree) Bool) -(assert-propagation ((?x1 nat)) (((leaf ?x1))) () () (= (is_leaf (leaf ?x1)) true) ) -(assert-propagation ((?x1 tree)) (((data ?x1))) () ((is_leaf ?x1)) (= ?x1 (leaf (data ?x1))) ) -(assert-propagation ((?x1 tree)) (((children ?x1))) () ((is_leaf ?x1)) (= (children ?x1) null) ) - -;;; directrr -(assert-rewrite ((?x1 list)) () () (is_node (node ?x1)) true ) -(assert-rewrite ((?x1 list)) () () (is_leaf (node ?x1)) false ) -(assert-rewrite ((?x1 nat)) () () (is_leaf (leaf ?x1)) true ) -(assert-rewrite ((?x1 nat)) () () (is_node (leaf ?x1)) false ) - - -;;;;;;;;;;;;;;;;;;;; -;; distinct -(assert-propagation ((?x1 tree)) () () ((is_node ?x1)) (not (is_leaf ?x1)) ) -(assert-propagation ((?x1 tree)) () () ((is_leaf ?x1)) (not (is_node ?x1)) ) -(assert-propagation ((?x1 tree)) () () ((not (is_node ?x1))) (is_leaf ?x1) ) -(assert-propagation ((?x1 tree)) () () ((not (is_leaf ?x1))) (is_node ?x1) ) - -;;;;;;;;;;;;;;;;;;; -;; case-split -(assert-propagation ((?x1 tree)) (((children ?x1))) () () (or (is_node ?x1) (is_leaf ?x1)) ) -(assert-propagation ((?x1 tree)) (((data ?x1))) () () (or (is_node ?x1) (is_leaf ?x1)) ) - - -;;;;;;;;;;;;;;;;;; -;; non-cyclic -(declare-fun size_list (list) Real) -(declare-fun size_tree (tree) Real) -(assert-propagation ((?x1 tree) (?x2 list)) (((cons ?x1 ?x2))) () () (and (> (size_list (cons ?x1 ?x2)) (size_tree ?x1)) (> (size_list (cons ?x1 ?x2)) (size_list ?x2))) ) -(assert-propagation ((?x1 list)) (((node ?x1))) () () (> (size_tree (node ?x1)) (size_list ?x1)) ) -(assert-propagation ((?x1 nat)) (((leaf ?x1))) () () (> (size_tree (leaf ?x1)) (size_nat ?x1)) ) diff --git a/test/regress/regress0/rewriterules/length.smt2 b/test/regress/regress0/rewriterules/length.smt2 deleted file mode 100644 index b144d7745..000000000 --- a/test/regress/regress0/rewriterules/length.smt2 +++ /dev/null @@ -1,27 +0,0 @@ -; COMMAND-LINE: --rewrite-rules -(set-logic AUFLIA) -(set-info :status unsat) - -;; don't use a datatypes for currently focusing in uf -(declare-sort list 0) - -(declare-fun cons (Int list) list) -(declare-fun nil () list) - - -;;define length -(declare-fun length (list) Int) - -(assert (forall ((?l list)) (! (=> (= ?l nil) (= (length ?l) 0)) :rewrite-rule))) - -(assert (forall ((?e Int) (?l list)) (! (= (length (cons ?e ?l)) (+ (length ?l) 1)) :rewrite-rule))) - -;;(assert (forall ((?l list)) (=> (= ?l nil) (= (length ?l) 0)))) - -;;(assert (forall ((?e Int) (?l list) (?l2 list)) (=> (= ?l2 (cons ?e ?l)) (= (length ?l2) (+ (length ?l) 1))))) - - -(assert (not (= (length (cons 1 (cons 2 (cons 3 nil)))) 3))) - -(check-sat) -(exit) diff --git a/test/regress/regress0/rewriterules/length_gen_n.smt2 b/test/regress/regress0/rewriterules/length_gen_n.smt2 deleted file mode 100644 index 7da2f6777..000000000 --- a/test/regress/regress0/rewriterules/length_gen_n.smt2 +++ /dev/null @@ -1,46 +0,0 @@ -; COMMAND-LINE: --rewrite-rules -;; Same than length.smt2 but the nil case is not a rewrite rule -;; So here the rewrite rules have no guards length - -(set-logic AUFLIA) -(set-info :status unsat) - -;; don't use a datatypes for currently focusing in uf -(declare-sort list 0) - -(declare-fun cons (Int list) list) -(declare-fun nil () list) - - -;;define length -(declare-fun length (list) Int) - -(assert (= (length nil) 0)) - -(assert (forall ((?e Int) (?l list)) (! (= (length (cons ?e ?l)) (+ 1 (length ?l))) :rewrite-rule))) - -(declare-fun gen_cons (Int list) list) - -(assert (forall ((?n Int) (?l list)) (! (=> (= ?n 0) (= (gen_cons ?n ?l) ?l)) :rewrite-rule))) - -(assert (forall ((?n Int) (?l list)) (! (=> (> ?n 0) (= (gen_cons ?n ?l) - (gen_cons (- ?n 1) (cons 1 ?l)))) :rewrite-rule))) - - -;;(assert (not (forall ((?n Int)) (=> (>= ?n 0) (=> (= (length (gen_cons ?n nil)) ?n) (= (length (gen_cons (+ ?n 1) nil)) (+ ?n 1))) )))) - -;;(assert (not (forall ((?n Int) (?l list)) (=> (>= ?n 0) (=> (= (length ?l) ?n) (= (length (cons 1 ?l)) (+ ?n 1))) )))) - -;; (assert (not (forall ((?n Int)) (=> (>= ?n 0) (=> (= (length (gen_cons ?n nil)) ?n) (= (length (cons 1 (gen_cons ?n nil))) (+ ?n 1))) )))) - -;;(assert (not (forall ((?n Int)) (=> (>= ?n 0) (= (gen_cons (+ ?n 1) nil) (cons 1 (gen_cons ?n nil))) )))) - -(assert (not (forall ((?n Int)) (=> (>= ?n 0) (=> - (forall ((?l list)) (= (gen_cons ?n (cons 1 ?l)) (cons 1 (gen_cons ?n ?l)))) - (forall ((?l list)) (= (gen_cons (+ ?n 1) (cons 1 ?l)) (cons 1 (gen_cons (+ ?n 1) ?l)))) - ))))) - - -(check-sat) - -(exit) diff --git a/test/regress/regress0/rewriterules/length_gen_n_lemma.smt2 b/test/regress/regress0/rewriterules/length_gen_n_lemma.smt2 deleted file mode 100644 index 7d65356ad..000000000 --- a/test/regress/regress0/rewriterules/length_gen_n_lemma.smt2 +++ /dev/null @@ -1,44 +0,0 @@ -; COMMAND-LINE: --rewrite-rules -;; Same than length.smt2 but the nil case is not a rewrite rule -;; So here the rewrite rules have no guards length - -(set-logic AUFLIA) -(set-info :status unsat) - -;; don't use a datatypes for currently focusing in uf -(declare-sort list 0) - -(declare-fun cons (Int list) list) -(declare-fun nil () list) - - -;;define length -(declare-fun length (list) Int) - -(assert (= (length nil) 0)) - -(assert (forall ((?e Int) (?l list)) (= (length (cons ?e ?l)) (+ 1 (length ?l))))) - -(declare-fun gen_cons (Int list) list) - -(assert (forall ((?n Int) (?l list)) (=> (= ?n 0) (= (gen_cons ?n ?l) ?l)))) - -(assert (forall ((?n Int) (?l list)) (=> (> ?n 0) (= (gen_cons ?n ?l) - (gen_cons (- ?n 1) (cons 1 ?l)))))) - - -;;(assert (not (forall ((?n Int)) (=> (>= ?n 0) (=> (= (length (gen_cons ?n nil)) ?n) (= (length (gen_cons (+ ?n 1) nil)) (+ ?n 1))) )))) - -;;(assert (not (forall ((?n Int) (?l list)) (=> (>= ?n 0) (=> (= (length ?l) ?n) (= (length (cons 1 ?l)) (+ ?n 1))) )))) - -;;(assert (not (forall ((?n Int)) (=> (>= ?n 0) (=> (= (length (gen_cons ?n nil)) ?n) (= (length (cons 1 (gen_cons ?n nil))) (+ ?n 1))) )))) - -(assert (not (forall ((?n Int)) (=> (>= ?n 0) (=> - (forall ((?l list)) (= (gen_cons ?n (cons 1 ?l)) (cons 1 (gen_cons ?n ?l)))) - (forall ((?l list)) (= (gen_cons (+ ?n 1) (cons 1 ?l)) (cons 1 (gen_cons (+ ?n 1) ?l)))) - ))))) - - -(check-sat) - -(exit) diff --git a/test/regress/regress0/rewriterules/length_trick.smt2 b/test/regress/regress0/rewriterules/length_trick.smt2 deleted file mode 100644 index e01e97b84..000000000 --- a/test/regress/regress0/rewriterules/length_trick.smt2 +++ /dev/null @@ -1,33 +0,0 @@ -; COMMAND-LINE: --rewrite-rules -;; Same than length.smt2 but the nil case is not a rewrite rule -;; So here the rewrite rules have no guards length - -(set-logic AUFLIA) -(set-info :status unsat) - -;; don't use a datatypes for currently focusing in uf -(declare-sort list 0) - -(declare-fun cons (Int list) list) -(declare-fun nil () list) - - -;;define length -(declare-fun length (list) Int) - -(assert (= (length nil) 0)) - - - - -(assert (forall ((?e Int) (?l list)) (! (= (length (cons ?e ?l)) (+ (length ?l) 1)) :rewrite-rule))) - -;;(assert (forall ((?l list)) (=> (= ?l nil) (= (length ?l) 0)))) - -;;(assert (forall ((?e Int) (?l list) (?l2 list)) (=> (= ?l2 (cons ?e ?l)) (= (length ?l2) (+ (length ?l) 1))))) - - -(assert (not (= (length (cons 1 (cons 2 (cons 3 nil)))) 3))) - -(check-sat) -(exit) diff --git a/test/regress/regress0/rewriterules/length_trick2.smt2 b/test/regress/regress0/rewriterules/length_trick2.smt2 deleted file mode 100644 index 8d47d9550..000000000 --- a/test/regress/regress0/rewriterules/length_trick2.smt2 +++ /dev/null @@ -1,33 +0,0 @@ -; COMMAND-LINE: --rewrite-rules -;; Same than length.smt2 but the nil case is not a rewrite rule -;; So here the rewrite rules have no guards length - -(set-logic AUFLIA) -(set-info :status unsat) - -;; don't use a datatypes for currently focusing in uf -(declare-sort list 0) - -(declare-fun cons (Int list) list) -(declare-fun nil () list) - - -;;define length -(declare-fun length (list) Int) - -(assert (= (length nil) 0)) - - - - -(assert (forall ((?e Int) (?l list)) (! (= (length (cons ?e ?l)) (+ (length ?l) 1)) :rewrite-rule))) - -;;(assert (forall ((?l list)) (=> (= ?l nil) (= (length ?l) 0)))) - -;;(assert (forall ((?e Int) (?l list) (?l2 list)) (=> (= ?l2 (cons ?e ?l)) (= (length ?l2) (+ (length ?l) 1))))) - -(assert (forall ((?a Int) (?b Int) (?l list)) - (not (> (length (cons ?a (cons ?b ?l))) (length ?l))))) -(check-sat) - -(exit) diff --git a/test/regress/regress0/rewriterules/native_arrays.smt2 b/test/regress/regress0/rewriterules/native_arrays.smt2 deleted file mode 100644 index 83de7d8f4..000000000 --- a/test/regress/regress0/rewriterules/native_arrays.smt2 +++ /dev/null @@ -1,35 +0,0 @@ -; COMMAND-LINE: --rewrite-rules -;; This example can't be done if we don't access the EqualityEngine of -;; the theory of arrays - -(set-logic AUFLIA) -(set-info :status unsat) - -(declare-sort Index 0) -(declare-sort Element 0) - -;;A dumb predicate for a simple example -(declare-fun P (Element) Bool) - -(assert-rewrite ((?i1 Index) (?i2 Index) (?e Element) (?a (Array Index Element))) () () - (P (select (store ?a ?i1 ?e) ?i2)) true ) - -(declare-fun a1 () (Array Index Element)) -(declare-fun a2 () (Array Index Element)) -(declare-fun a3 () (Array Index Element)) -(declare-fun i1 () Index) -(declare-fun i2 () Index) -(declare-fun e1 () Element) - -(assert (not (=> (or (= a1 (store a2 i1 e1)) (= a1 (store a3 i1 e1))) (P (select a1 i2)) ))) -(check-sat) -(exit) - - -;; (declare-fun a1 () (Array Index Element)) -;; (declare-fun a2 () (Array Index Element)) -;; (declare-fun i1 () Index) -;; (assert (= (store a1 i1 (select a2 i1)) (store a2 i1 (select a1 i1)))) -;; (assert (not (= a1 a2))) -;; (check-sat) -;; (exit) diff --git a/test/regress/regress0/rewriterules/native_datatypes.smt2 b/test/regress/regress0/rewriterules/native_datatypes.smt2 deleted file mode 100644 index 365ec0624..000000000 --- a/test/regress/regress0/rewriterules/native_datatypes.smt2 +++ /dev/null @@ -1,34 +0,0 @@ -; COMMAND-LINE: --rewrite-rules -;; Same than length.smt2 but the nil case is not a rewrite rule -;; So here the rewrite rules have no guards length - -(set-info :status unsat) - -(declare-datatypes ((nat 0) (list 0)) ( -((succ (pred nat)) (zero ) ) -((cons (car nat)(cdr list)) (nil ) ) - -)) - - -;;define length -(declare-fun length (list) nat) - -(assert (= (length nil) zero)) - -(assert (forall ((?e nat) (?l list)) (! (= (length (cons ?e ?l)) (succ (length ?l))) :rewrite-rule))) - -(declare-fun gen_cons (nat list) list) - -(assert (forall ((?l list)) (! (= (gen_cons zero ?l) ?l) :rewrite-rule))) - -(assert (forall ((?n nat) (?l list)) (! (= (gen_cons (succ ?n) ?l) - (gen_cons ?n (cons zero ?l))) :rewrite-rule))) - -(declare-fun n () nat) - -(assert (not (= (length (gen_cons (succ (succ zero)) nil)) (succ (succ zero))))) - -(check-sat) - -(exit) diff --git a/test/regress/regress0/rewriterules/relation.smt2 b/test/regress/regress0/rewriterules/relation.smt2 deleted file mode 100644 index 6b55a9677..000000000 --- a/test/regress/regress0/rewriterules/relation.smt2 +++ /dev/null @@ -1,28 +0,0 @@ -; COMMAND-LINE: --rewrite-rules -(set-logic AUFLIA) -(set-info :status unsat) - -;; don't use a datatypes for currently focusing in uf -(declare-sort elt 0) - -(declare-fun R (elt elt) Bool) - -;; reflexive -(assert-rewrite ((x elt)) () () (R x x) true) - -;; transitive -(assert-propagation ((x elt) (y elt) (z elt)) () () ((R x y) (R y z)) (R x z)) - -;; anti-symmetric -(assert-propagation ((x elt) (y elt)) () () ((R x y) (R y x)) (= x y)) - -(declare-fun e1 () elt) -(declare-fun e2 () elt) -(declare-fun e3 () elt) -(declare-fun e4 () elt) - -(assert (not (=> (and (R e1 e2) (R e2 e3) (R e3 e4) (R e4 e1)) (= e1 e4)))) - -(check-sat) - -(exit) \ No newline at end of file diff --git a/test/regress/regress0/rewriterules/simulate_rewriting.smt2 b/test/regress/regress0/rewriterules/simulate_rewriting.smt2 deleted file mode 100644 index f67a0e6a2..000000000 --- a/test/regress/regress0/rewriterules/simulate_rewriting.smt2 +++ /dev/null @@ -1,25 +0,0 @@ -; COMMAND-LINE: --rewrite-rules -;; A new fast tableau-base ... Domenico Cantone et Calogero G.Zarba -(set-logic AUFLIA) -(set-info :status unsat) - -(declare-sort elt1 0) -(declare-sort elt2 0) - -(declare-fun g (elt2) Bool) - -(declare-fun p (elt1 elt1) Bool) -(declare-fun f (elt2) elt1) -(declare-fun c1 () elt1) -(declare-fun c2 () elt1) - -(assert (forall ((?e elt2)) (! (=> (g ?e) (= (f ?e) c2)) :rewrite-rule))) -(assert (forall ((?e elt2)) (! (=> (g ?e) (= (f ?e) c1)) :rewrite-rule))) - -(declare-fun e () elt2) - -(assert (not (=> (g e) (=> (p c1 c2) (p (f e) (f e)))) )) - -(check-sat) - -(exit) diff --git a/test/regress/regress1/push-pop/bug326.smt2 b/test/regress/regress1/push-pop/bug326.smt2 deleted file mode 100644 index f1506b3e8..000000000 --- a/test/regress/regress1/push-pop/bug326.smt2 +++ /dev/null @@ -1,41 +0,0 @@ -; COMMAND-LINE: --incremental --rewrite-rules - -(set-logic AUFLIA) - -(declare-fun R (Int Int) Bool) - -;; reflexive -(assert-rewrite ((x Int)) () () (R x x) true) - -;; anti-symmetric -(assert-reduction ((x Int) (y Int)) () () ((R x y) (R y x)) (= x y)) - -;; transitive -(assert-propagation ((x Int) (y Int) (z Int)) () () ((R x y) (R y z)) (R x z)) - - -(declare-fun e1 () Int) -(declare-fun e2 () Int) -(declare-fun e3 () Int) -(declare-fun e4 () Int) - -; EXPECT: unsat -(push);;unsat -(assert (not (=> (and (R e1 e2) (R e2 e4) (R e1 e3) (R e3 e4) (= e1 e4)) (= e2 e3)))) -(check-sat) -(pop) - -; EXPECT: unsat -(push);;unsat -(assert (not (=> (and (R e1 e2) (R e1 e3) (or (R e2 e4) (R e3 e4)) ) (R e1 e4)))) -(check-sat) -(pop) - -; EXPECT: sat -(push);;sat -(assert (and (not (R e1 e3)) (R e4 e1))) -(check-sat) -(pop) - - -(exit) diff --git a/test/regress/regress1/rewriterules/datatypes2.smt2 b/test/regress/regress1/rewriterules/datatypes2.smt2 deleted file mode 100644 index 4ef40597a..000000000 --- a/test/regress/regress1/rewriterules/datatypes2.smt2 +++ /dev/null @@ -1,151 +0,0 @@ -; COMMAND-LINE: --rewrite-rules -;; try to solve datatypes with rewriterules -(set-logic AUFLIA) -(set-info :status unsat) - -;; lists 2 nil -(declare-sort elt 0) ;; we suppose that elt is infinite -(declare-sort list 0) - -(declare-fun nil1 () list) -(declare-fun nil2 () list) -(declare-fun cons1 (elt list) list) -(declare-fun cons2 (elt list) list) - -;;;;;;;;;;;;;;;;;;;; -;; injective - -(declare-fun inj11 (list) elt) -(assert (forall ((?e elt) (?l list)) - (! (! (=> true (=> true (= (inj11 (cons1 ?e ?l)) ?e))) :pattern ((cons1 ?e ?l)) ) :rewrite-rule) )) - -(declare-fun inj12 (list) list) -(assert (forall ((?e elt) (?l list)) - (! (! (=> true (=> true (= (inj12 (cons1 ?e ?l)) ?l))) :pattern ((cons1 ?e ?l)) ) :rewrite-rule) )) - -(declare-fun inj21 (list) elt) -(assert (forall ((?e elt) (?l list)) - (! (! (=> true (=> true (= (inj21 (cons2 ?e ?l)) ?e))) :pattern ((cons2 ?e ?l)) ) :rewrite-rule) )) - -(declare-fun inj22 (list) list) -(assert (forall ((?e elt) (?l list)) - (! (! (=> true (=> true (= (inj22 (cons2 ?e ?l)) ?l))) :pattern ((cons2 ?e ?l)) ) :rewrite-rule) )) - - -;;;;;;;;;;;;;;;;;;;; -;; projection - -(declare-fun proj11 (list) elt) -(assert (forall ((?e elt) (?l list)) - (! (= (proj11 (cons1 ?e ?l)) ?e) :rewrite-rule) )) - -(declare-fun proj12 (list) list) -(assert (forall ((?e elt) (?l list)) - (! (= (proj12 (cons1 ?e ?l)) ?l) :rewrite-rule) )) - - -(declare-fun proj21 (list) elt) -(assert (forall ((?e elt) (?l list)) - (! (= (proj21 (cons2 ?e ?l)) ?e) :rewrite-rule) )) - -(declare-fun proj22 (list) list) -(assert (forall ((?e elt) (?l list)) - (! (= (proj22 (cons2 ?e ?l)) ?l) :rewrite-rule) )) - - -;;;;;;;;;;;;;;;;;;; -;; test -(declare-fun iscons1 (list) Bool) -(assert (= (iscons1 nil1) false)) -(assert (= (iscons1 nil2) false)) -(assert (forall ((?e elt) (?l list)) - (! (! (=> true (=> true (= (iscons1 (cons1 ?e ?l)) true))) :pattern ((cons1 ?e ?l)) ) :rewrite-rule) )) -(assert (forall ((?e elt) (?l list)) - (! (! (=> true (=> true (= (iscons1 (cons2 ?e ?l)) false))) :pattern ((cons2 ?e ?l)) ) :rewrite-rule) )) - -(assert (forall ((?l list)) - (! (! (=> true (=> (iscons1 ?l) (= ?l (cons1 (proj11 ?l) (proj12 ?l))))) :pattern ((proj11 ?l)) ) :rewrite-rule) )) -(assert (forall ((?l list)) - (! (! (=> true (=> (iscons1 ?l) (= ?l (cons1 (proj11 ?l) (proj12 ?l))))) :pattern ((proj12 ?l)) ) :rewrite-rule) )) - - -(declare-fun iscons2 (list) Bool) -(assert (= (iscons2 nil1) false)) -(assert (= (iscons2 nil2) false)) -(assert (forall ((?e elt) (?l list)) - (! (! (=> true (=> true (= (iscons2 (cons1 ?e ?l)) false))) :pattern ((cons1 ?e ?l)) ) :rewrite-rule) )) -(assert (forall ((?e elt) (?l list)) - (! (! (=> true (=> true (= (iscons2 (cons2 ?e ?l)) true))) :pattern ((cons2 ?e ?l)) ) :rewrite-rule) )) - -(assert (forall ((?l list)) - (! (! (=> true (=> (iscons2 ?l) (= ?l (cons2 (proj21 ?l) (proj22 ?l))))) :pattern ((proj21 ?l)) ) :rewrite-rule) )) -(assert (forall ((?l list)) - (! (! (=> true (=> (iscons2 ?l) (= ?l (cons2 (proj21 ?l) (proj22 ?l))))) :pattern ((proj22 ?l)) ) :rewrite-rule) )) - - -(declare-fun isnil1 (list) Bool) -(assert (= (isnil1 nil1) true)) -(assert (= (isnil1 nil2) false)) -(assert (forall ((?e elt) (?l list)) - (! (= (isnil1 (cons1 ?e ?l)) false) :rewrite-rule) )) -(assert (forall ((?e elt) (?l list)) - (! (= (isnil1 (cons2 ?e ?l)) false) :rewrite-rule) )) -(assert (forall ((?l list)) - (! (=> true (=> (isnil1 ?l) (= ?l nil1))) :rewrite-rule) )) - -(declare-fun isnil2 (list) Bool) -(assert (= (isnil2 nil1) false)) -(assert (= (isnil2 nil2) true)) -(assert (forall ((?e elt) (?l list)) - (! (= (isnil2 (cons1 ?e ?l)) false) :rewrite-rule) )) -(assert (forall ((?e elt) (?l list)) - (! (= (isnil2 (cons2 ?e ?l)) false) :rewrite-rule) )) -(assert (forall ((?l list)) - (! (=> true (=> (isnil2 ?l) (= ?l nil2))) :rewrite-rule) )) - -;; distinct -(assert (forall ((?l list)) - (! (=> (isnil1 ?l) (and (not (isnil2 ?l)) (not (iscons1 ?l)) (not (iscons2 ?l))) ) :rewrite-rule) )) - -(assert (forall ((?l list)) - (! (=> (isnil2 ?l) (and (not (isnil1 ?l)) (not (iscons1 ?l)) (not (iscons2 ?l))) ) :rewrite-rule) )) - -(assert (forall ((?l list)) - (! (=> (iscons1 ?l) (and (not (isnil1 ?l)) (not (isnil2 ?l)) (not (iscons2 ?l))) ) :rewrite-rule) )) - -(assert (forall ((?l list)) - (! (=> (iscons2 ?l) (and (not (isnil1 ?l)) (not (isnil2 ?l)) (not (iscons1 ?l))) ) :rewrite-rule) )) - - -;;;;;;;;;;;;;;;;;;; -;; case-split -(assert (forall ((?l list)) - (! (! (=> true (or (isnil1 ?l) (isnil2 ?l) (iscons1 ?l) (iscons2 ?l))) :pattern ((proj11 ?l)) ) :rewrite-rule) )) -(assert (forall ((?l list)) - (! (! (=> true (or (isnil1 ?l) (isnil2 ?l) (iscons1 ?l) (iscons2 ?l))) :pattern ((proj12 ?l)) ) :rewrite-rule) )) -(assert (forall ((?l list)) - (! (! (=> true (or (isnil1 ?l) (isnil2 ?l) (iscons1 ?l) (iscons2 ?l))) :pattern ((proj21 ?l)) ) :rewrite-rule) )) -(assert (forall ((?l list)) - (! (! (=> true (or (isnil1 ?l) (isnil2 ?l) (iscons1 ?l) (iscons2 ?l))) :pattern ((proj22 ?l)) ) :rewrite-rule) )) - -;;;;;;;;;;;;;;;;;;; -;; finite case-split -(assert (forall ((?l list)) - (! (=> (and (not (iscons1 ?l)) (not (iscons2 ?l))) (or (isnil1 ?l) (isnil2 ?l))) :rewrite-rule) )) - - - -;;;;; goal - -(declare-fun e () elt) -(declare-fun l1 () list) -(declare-fun l2 () list) - - - (assert (not (=> (iscons2 l1) (=> (= (proj22 l1) (proj22 l2)) (= l1 (cons2 (proj21 l1) (proj22 l2))))))) - -;;(assert (= (cons1 l1 l2) (cons2 l1 l2))) - -(check-sat) - -(exit) diff --git a/test/regress/regress1/rewriterules/datatypes3.smt2 b/test/regress/regress1/rewriterules/datatypes3.smt2 deleted file mode 100644 index fb9d79121..000000000 --- a/test/regress/regress1/rewriterules/datatypes3.smt2 +++ /dev/null @@ -1,138 +0,0 @@ -; COMMAND-LINE: --rewrite-rules -;; try to solve datatypes with rewriterules -(set-logic AUFLIA) -(set-info :status unsat) - -;; lists 2 nil -(declare-sort elt 0) ;; we suppose that elt is infinite -(declare-sort list 0) - -(declare-fun nil1 () list) -(declare-fun nil2 () list) -(declare-fun cons1 (elt list) list) -(declare-fun cons2 (elt list) list) - -;;;;;;;;;;;;;;;;;;;; -;; injective - -(declare-fun inj11 (list) elt) -(assert (forall ((?e elt) (?l list)) - (! (! (=> true (=> true (= (inj11 (cons1 ?e ?l)) ?e))) :pattern ((cons1 ?e ?l)) ) :rewrite-rule) )) - -(declare-fun inj12 (list) list) -(assert (forall ((?e elt) (?l list)) - (! (! (=> true (=> true (= (inj12 (cons1 ?e ?l)) ?l))) :pattern ((cons1 ?e ?l)) ) :rewrite-rule) )) - -(declare-fun inj21 (list) elt) -(assert (forall ((?e elt) (?l list)) - (! (! (=> true (=> true (= (inj21 (cons2 ?e ?l)) ?e))) :pattern ((cons2 ?e ?l)) ) :rewrite-rule) )) - -(declare-fun inj22 (list) list) -(assert (forall ((?e elt) (?l list)) - (! (! (=> true (=> true (= (inj22 (cons2 ?e ?l)) ?l))) :pattern ((cons2 ?e ?l)) ) :rewrite-rule) )) - - -;;;;;;;;;;;;;;;;;;;; -;; projection - -(declare-fun proj11 (list) elt) -(assert (forall ((?e elt) (?l list)) - (! (= (proj11 (cons1 ?e ?l)) ?e) :rewrite-rule) )) - -(declare-fun proj12 (list) list) -(assert (forall ((?e elt) (?l list)) - (! (= (proj12 (cons1 ?e ?l)) ?l) :rewrite-rule) )) - -(assert (= (proj11 nil1) nil1)) -(assert (= (proj12 nil1) nil1)) -(assert (= (proj11 nil2) nil2)) -(assert (= (proj12 nil2) nil2)) - -(declare-fun proj21 (list) elt) -(assert (forall ((?e elt) (?l list)) - (! (= (proj21 (cons2 ?e ?l)) ?e) :rewrite-rule) )) - -(declare-fun proj22 (list) list) -(assert (forall ((?e elt) (?l list)) - (! (= (proj22 (cons2 ?e ?l)) ?l) :rewrite-rule) )) - -(assert (= (proj21 nil1) nil1)) -(assert (= (proj22 nil1) nil1)) -(assert (= (proj21 nil2) nil2)) -(assert (= (proj22 nil2) nil2)) - - -;;;;;;;;;;;;;;;;;;; -;; test -(declare-fun iscons1 (list) Bool) -(assert (forall ((?e elt) (?l list)) - (! (! (=> true (=> true (= (iscons1 (cons1 ?e ?l)) true))) :pattern ((cons1 ?e ?l)) ) :rewrite-rule) )) - -(assert (forall ((?l list)) - (! (! (=> true (=> (iscons1 ?l) (= ?l (cons1 (proj11 ?l) (proj12 ?l))))) :pattern ((proj11 ?l)) ) :rewrite-rule) )) -(assert (forall ((?l list)) - (! (! (=> true (=> (iscons1 ?l) (= ?l (cons1 (proj11 ?l) (proj12 ?l))))) :pattern ((proj12 ?l)) ) :rewrite-rule) )) - - -(declare-fun iscons2 (list) Bool) -(assert (forall ((?e elt) (?l list)) - (! (! (=> true (=> true (= (iscons2 (cons2 ?e ?l)) true))) :pattern ((cons2 ?e ?l)) ) :rewrite-rule) )) - -(assert (forall ((?l list)) - (! (! (=> true (=> (iscons2 ?l) (= ?l (cons2 (proj21 ?l) (proj22 ?l))))) :pattern ((proj21 ?l)) ) :rewrite-rule) )) -(assert (forall ((?l list)) - (! (! (=> true (=> (iscons2 ?l) (= ?l (cons2 (proj21 ?l) (proj22 ?l))))) :pattern ((proj22 ?l)) ) :rewrite-rule) )) - - -(declare-fun isnil1 (list) Bool) -(assert (= (isnil1 nil1) true)) - -(declare-fun isnil2 (list) Bool) -(assert (= (isnil2 nil2) true)) - -;; distinct -(assert (forall ((?l list)) - (! (=> (isnil1 ?l) (and (not (isnil2 ?l)) (not (iscons1 ?l)) (not (iscons2 ?l))) ) :rewrite-rule) )) - -(assert (forall ((?l list)) - (! (=> (isnil2 ?l) (and (not (isnil1 ?l)) (not (iscons1 ?l)) (not (iscons2 ?l))) ) :rewrite-rule) )) - -(assert (forall ((?l list)) - (! (=> (iscons1 ?l) (and (not (isnil1 ?l)) (not (isnil2 ?l)) (not (iscons2 ?l))) ) :rewrite-rule) )) - -(assert (forall ((?l list)) - (! (=> (iscons2 ?l) (and (not (isnil1 ?l)) (not (isnil2 ?l)) (not (iscons1 ?l))) ) :rewrite-rule) )) - - -;;;;;;;;;;;;;;;;;;; -;; case-split -(assert (forall ((?l list)) - (! (! (=> true (or (isnil1 ?l) (isnil2 ?l) (iscons1 ?l) (iscons2 ?l))) :pattern ((proj11 ?l)) ) :rewrite-rule) )) -(assert (forall ((?l list)) - (! (! (=> true (or (isnil1 ?l) (isnil2 ?l) (iscons1 ?l) (iscons2 ?l))) :pattern ((proj12 ?l)) ) :rewrite-rule) )) -(assert (forall ((?l list)) - (! (! (=> true (or (isnil1 ?l) (isnil2 ?l) (iscons1 ?l) (iscons2 ?l))) :pattern ((proj21 ?l)) ) :rewrite-rule) )) -(assert (forall ((?l list)) - (! (! (=> true (or (isnil1 ?l) (isnil2 ?l) (iscons1 ?l) (iscons2 ?l))) :pattern ((proj22 ?l)) ) :rewrite-rule) )) - -;;;;;;;;;;;;;;;;;;; -;; finite case-split -(assert (forall ((?l list)) - (! (=> (and (not (iscons1 ?l)) (not (iscons2 ?l))) (or (isnil1 ?l) (isnil2 ?l))) :rewrite-rule) )) - - - -;;;;; goal - -(declare-fun e () elt) -(declare-fun l1 () list) -(declare-fun l2 () list) - - -;; (assert (not (=> (iscons2 l1) (=> (= (proj22 l1) (proj22 l2)) (= l1 (cons2 (proj21 l1) (proj22 l2))))))) - -(assert (= (cons1 l1 l2) (cons2 l1 l2))) - -(check-sat) - -(exit) diff --git a/test/regress/regress1/rewriterules/datatypes_clark_quantification.smt2 b/test/regress/regress1/rewriterules/datatypes_clark_quantification.smt2 deleted file mode 100644 index a8dc5227a..000000000 --- a/test/regress/regress1/rewriterules/datatypes_clark_quantification.smt2 +++ /dev/null @@ -1,265 +0,0 @@ -; COMMAND-LINE: --rewrite-rules -(set-logic AUFLIRA) - -;; DATATYPE -;; nat = succ(pred : nat) | zero, -;; list = cons(car : tree, cdr : list) | null, -;; tree = node(children : list) | leaf(data : nat) -;; END; - -;;;;;;;;;;; -;; nat ;; -;;;;;;;;;;; -(declare-sort nat 0) -(declare-fun zero () nat) -(declare-fun succ (nat) nat) - -;;;;;;;;;;;;;;;; -;; injective - -(declare-fun inj1 (nat) nat) -(assert (forall ((?x1 nat)) - (! (= (inj1 (succ ?x1)) ?x1) :pattern ((succ ?x1)) ) )) - - -;;;;;;;;;;;;;;;;;;;; -;; projection - -(declare-fun pred (nat) nat) -(assert (forall ((?x1 nat)) - (! (= (pred (succ ?x1)) ?x1) :pattern ((pred (succ ?x1))) ) )) - -(assert (= (pred zero) zero)) - -;;;;;;;;;;;;;;;;;;; -;; test -(declare-fun is_succ (nat) Bool) -(assert (= (is_succ zero) false)) -(assert (forall ((?x1 nat)) - (! (= (is_succ (succ ?x1)) true) :pattern ((succ ?x1)) ) )) - -(assert (forall ((?x1 nat)) - (! (=> (is_succ ?x1) (= ?x1 (succ (pred ?x1)))) :pattern ((is_succ ?x1) (pred ?x1)) ) )) - -(declare-fun is_zero (nat) Bool) -(assert (= (is_zero zero) true)) -(assert (forall ((?x1 nat)) - (! (=> (is_zero ?x1) (= ?x1 zero)) :pattern ((is_zero ?x1)) ) )) - -;;; directrr -(assert (forall ((?x1 nat)) - (! (= (is_succ (succ ?x1)) true) :pattern ((is_succ (succ ?x1))) ) )) -(assert (forall ((?x1 nat)) - (! (= (is_zero (succ ?x1)) false) :pattern ((is_zero (succ ?x1))) ))) - - -;;;;;;;;;;;;;;;;;;;; -;; distinct -(assert (forall ((?x1 nat)) - (! (=> (is_zero ?x1) (not (is_succ ?x1)) ) :pattern ((is_zero ?x1)) ) )) -(assert (forall ((?x1 nat)) - (! (=> (is_succ ?x1) (not (is_zero ?x1)) ) :pattern ((is_succ ?x1)) ) )) -(assert (forall ((?x1 nat)) - (! (=> (not (is_zero ?x1)) (is_succ ?x1) ) :pattern ((is_zero ?x1)) ) )) -(assert (forall ((?x1 nat)) - (! (=> (not (is_succ ?x1)) (is_zero ?x1) ) :pattern ((is_succ ?x1)) ) )) - -;;;;;;;;;;;;;;;;;;; -;; case-split -(assert (forall ((?x1 nat)) - (! (or (is_zero ?x1) (is_succ ?x1)) :pattern ((pred ?x1)) ) )) - -;;;;;;;;;;;;;;;;;;; -;; non-cyclic -(declare-fun size_nat (nat) Real) -(assert (forall ((?x1 nat)) - (! (> (size_nat (succ ?x1)) (size_nat ?x1)) :pattern ((succ ?x1)) ) )) - - - -;;;;;;;;;;;;;;;;;;;;; -;; list and tree - -(declare-sort list 0) -(declare-sort tree 0) - -;;;;;;;;;;; -;; list ;; -;;;;;;;;;;; - -(declare-fun null () list) -(declare-fun cons (tree list) list) - -(declare-fun node (list) tree) -(declare-fun leaf (nat) tree) - -;;;;;;;;;;;;;;;; -;; injective - -(declare-fun inj2 (list) tree) -(assert (forall ((?x1 tree) (?x2 list)) - (! (= (inj2 (cons ?x1 ?x2)) ?x1) :pattern ((cons ?x1 ?x2)) ) )) - -(declare-fun inj3 (list) list) -(assert (forall ((?x1 tree) (?x2 list)) - (! (= (inj3 (cons ?x1 ?x2)) ?x2) :pattern ((cons ?x1 ?x2)) ) )) - - -;;;;;;;;;;;;;;;;;;;; -;; projection - -(declare-fun car (list) tree) -(assert (forall ((?x1 tree) (?x2 list)) - (! (= (car (cons ?x1 ?x2)) ?x1) :pattern ((car (cons ?x1 ?x2))) ) )) - -(assert (= (car null) (node null))) - -(declare-fun cdr (list) list) -(assert (forall ((?x1 tree) (?x2 list)) - (! (= (cdr (cons ?x1 ?x2)) ?x2) :pattern ((cdr (cons ?x1 ?x2))) ) )) - -(assert (= (cdr null) null)) - -;;;;;;;;;;;;;;;;;;; -;; test -(declare-fun is_cons (list) Bool) -(assert (= (is_cons null) false)) -(assert (forall ((?x1 tree) (?x2 list)) - (! (= (is_cons (cons ?x1 ?x2)) true) :pattern ((cons ?x1 ?x2)) ) )) - -(assert (forall ((?x1 list)) - (! (=> (is_cons ?x1) (= ?x1 (cons (car ?x1) (cdr ?x1)))) :pattern ((is_cons ?x1)(car ?x1)) ) )) -(assert (forall ((?x1 list)) - (! (=> (is_cons ?x1) (= ?x1 (cons (car ?x1) (cdr ?x1)))) :pattern ((is_cons ?x1)(cdr ?x1)) ) )) - -(declare-fun is_null (list) Bool) -(assert (= (is_null null) true)) - -(assert (forall ((?x1 list)) - (! (=> (is_null ?x1) (= (car ?x1) (node null))) :pattern ((is_null ?x1)(car ?x1)) ) )) -(assert (forall ((?x1 list)) - (! (=> (is_null ?x1) (= (cdr ?x1) null)) :pattern ((is_null ?x1)(cdr ?x1)) ) )) - -(assert (forall ((?x1 list)) - (! (=> (is_null ?x1) (= ?x1 null)) :pattern ((is_null ?x1)) ) )) - -;;; directrr -(assert (forall ((?x1 tree) (?x2 list)) - (! (= (is_cons (cons ?x1 ?x2)) true) :pattern ((is_cons (cons ?x1 ?x2))) ) )) -(assert (forall ((?x1 tree) (?x2 list)) - (! (= (is_null (cons ?x1 ?x2)) false) :pattern ((is_null (cons ?x1 ?x2))) ) )) - - - -;;;;;;;;;;;;;;;;;;;; -;; distinct -(assert (forall ((?x1 list)) - (! (=> (is_null ?x1) (not (is_cons ?x1)) ) :pattern ((is_null ?x1)) ) )) -(assert (forall ((?x1 list)) - (! (=> (is_cons ?x1) (not (is_null ?x1)) ) :pattern ((is_cons ?x1)) ) )) -(assert (forall ((?x1 list)) - (! (=> (not (is_null ?x1)) (is_cons ?x1) ) :pattern ((is_null ?x1)) ) )) -(assert (forall ((?x1 list)) - (! (=> (not (is_cons ?x1)) (is_null ?x1) ) :pattern ((is_cons ?x1)) ) )) - -;;;;;;;;;;;;;;;;;;; -;; case-split -(assert (forall ((?x1 list)) - (! (or (is_null ?x1) (is_cons ?x1)) :pattern ((car ?x1)) ) )) -(assert (forall ((?x1 list)) - (! (or (is_null ?x1) (is_cons ?x1)) :pattern ((cdr ?x1)) ) )) - -;;;;;;;;;;;;;;; -;; tree - -;;;;;;;;;;;;;;;; -;; injective - -(declare-fun inj4 (tree) list) -(assert (forall ((?x1 list)) - (! (= (inj4 (node ?x1)) ?x1) :pattern ((node ?x1)) ) )) - -(declare-fun inj5 (tree) nat) -(assert (forall ((?x1 nat)) - (! (= (inj5 (leaf ?x1)) ?x1) :pattern ((leaf ?x1)) ) )) - - -;;;;;;;;;;;;;;;;;;;; -;; projection - -(declare-fun children (tree) list) -(assert (forall ((?x1 list)) - (! (= (children (node ?x1)) ?x1) :pattern ((children (node ?x1))) ) )) -(assert (forall ((?x1 nat)) - (! (= (children (leaf ?x1)) null) :pattern ((children (leaf ?x1))) ) )) - - -(declare-fun data (tree) nat) -(assert (forall ((?x1 nat)) - (! (= (data (leaf ?x1)) ?x1) :pattern ((data (leaf ?x1))) ) )) -(assert (forall ((?x1 list)) - (! (= (data (node ?x1)) zero) :pattern ((data (node ?x1))) ) )) - -;;;;;;;;;;;;;;;;;;; -;; test -(declare-fun is_node (tree) Bool) -(assert (forall ((?x1 list)) - (! (= (is_node (node ?x1)) true) :pattern ((node ?x1)) ) )) - -(assert (forall ((?x1 tree)) - (! (=> (is_node ?x1) (= ?x1 (node (children ?x1)))) :pattern ((is_node ?x1)(children ?x1)) ) )) - -(assert (forall ((?x1 tree)) - (! (=> (is_node ?x1) (= (data ?x1) zero)) :pattern ((is_node ?x1)(data ?x1)) ) )) - - -(declare-fun is_leaf (tree) Bool) -(assert (forall ((?x1 nat)) - (! (=> true (= (is_leaf (leaf ?x1)) true)) :pattern ((leaf ?x1)) ) )) - -(assert (forall ((?x1 tree)) - (! (=> (is_leaf ?x1) (= ?x1 (leaf (data ?x1)))) :pattern ((is_leaf ?x1)(data ?x1)) ) )) -(assert (forall ((?x1 tree)) - (! (=> (is_leaf ?x1) (= (children ?x1) null)) :pattern ((is_leaf ?x1)(children ?x1)) ) )) - -;;; directrr -(assert (forall ((?x1 list)) - (! (= (is_node (node ?x1)) true) :pattern ((is_node (node ?x1))) ) )) -(assert (forall ((?x1 list)) - (! (= (is_leaf (node ?x1)) false) :pattern ((is_leaf (node ?x1))) ) )) -(assert (forall ((?x1 nat)) - (! (= (is_leaf (leaf ?x1)) true) :pattern (is_leaf (leaf ?x1)) ) )) -(assert (forall ((?x1 nat)) - (! (= (is_node (leaf ?x1)) false) :pattern ((is_node (leaf ?x1))) ) )) - - -;;;;;;;;;;;;;;;;;;;; -;; distinct -(assert (forall ((?x1 tree)) - (! (=> (is_node ?x1) (not (is_leaf ?x1)) ) :pattern ((is_node ?x1)) ) )) -(assert (forall ((?x1 tree)) - (! (=> (is_leaf ?x1) (not (is_node ?x1)) ) :pattern ((is_leaf ?x1)) ) )) -(assert (forall ((?x1 tree)) - (! (=> (not (is_node ?x1)) (is_leaf ?x1) ) :pattern ((is_node ?x1)) ) )) -(assert (forall ((?x1 tree)) - (! (=> (not (is_leaf ?x1)) (is_node ?x1) ) :pattern ((is_leaf ?x1)) ) )) - -;;;;;;;;;;;;;;;;;;; -;; case-split -(assert (forall ((?x1 tree)) - (! (or (is_node ?x1) (is_leaf ?x1)) :pattern ((children ?x1)) ) )) - -(assert (forall ((?x1 tree)) - (! (or (is_node ?x1) (is_leaf ?x1)) :pattern ((data ?x1)) ) )) - - -;;;;;;;;;;;;;;;;;; -;; non-cyclic -(declare-fun size_list (list) Real) -(declare-fun size_tree (tree) Real) -(assert (forall ((?x1 tree) (?x2 list)) - (! (and (> (size_list (cons ?x1 ?x2)) (size_tree ?x1)) (> (size_list (cons ?x1 ?x2)) (size_list ?x2))) :pattern ((cons ?x1 ?x2)) ) )) -(assert (forall ((?x1 list)) - (! (> (size_tree (node ?x1)) (size_list ?x1)) :pattern ((node ?x1)) ) )) -(assert (forall ((?x1 nat)) - (! (> (size_tree (leaf ?x1)) (size_nat ?x1)) :pattern ((leaf ?x1)) ) )) diff --git a/test/regress/regress1/rewriterules/datatypes_sat.smt2 b/test/regress/regress1/rewriterules/datatypes_sat.smt2 deleted file mode 100644 index 4b5b59435..000000000 --- a/test/regress/regress1/rewriterules/datatypes_sat.smt2 +++ /dev/null @@ -1,102 +0,0 @@ -; COMMAND-LINE: --rewrite-rules --no-check-models -;; try to solve datatypes with rewriterules -(set-logic AUFLIA) -(set-info :status sat) - -;; lists 2 nil -(declare-sort elt 0) ;; we suppose that elt is infinite -(declare-sort list 0) - -(declare-fun nil1 () list) -(declare-fun nil2 () list) -(declare-fun cons (elt list) list) - -;;;;;;;;;;;;;;;;;;;; -;; injective - -(declare-fun inj1 (list) elt) -(assert (forall ((?e elt) (?l list)) - (! (! (=> true (=> true (= (inj1 (cons ?e ?l)) ?e))) :pattern ((cons ?e ?l)) ) :rewrite-rule) )) - -(declare-fun inj2 (list) list) -(assert (forall ((?e elt) (?l list)) - (! (! (=> true (=> true (= (inj2 (cons ?e ?l)) ?l))) :pattern ((cons ?e ?l)) ) :rewrite-rule) )) - -;;;;;;;;;;;;;;;;;;;; -;; projection - -(declare-fun proj1 (list) elt) -(assert (forall ((?e elt) (?l list)) - (! (= (proj1 (cons ?e ?l)) ?e) :rewrite-rule) )) - -(declare-fun proj2 (list) list) -(assert (forall ((?e elt) (?l list)) - (! (= (proj2 (cons ?e ?l)) ?l) :rewrite-rule) )) - -;;;;;;;;;;;;;;;;;;; -;; test -(declare-fun iscons (list) Bool) -(assert (= (iscons nil1) false)) -(assert (= (iscons nil2) false)) -(assert (forall ((?e elt) (?l list)) - (! (! (=> true (=> true (= (iscons (cons ?e ?l)) true))) :pattern ((cons ?e ?l)) ) :rewrite-rule) )) - -(assert (forall ((?l list)) - (! (! (=> true (=> (iscons ?l) (= ?l (cons (proj1 ?l) (proj2 ?l))))) :pattern ((proj1 ?l)) ) :rewrite-rule) )) -(assert (forall ((?l list)) - (! (! (=> true (=> (iscons ?l) (= ?l (cons (proj1 ?l) (proj2 ?l))))) :pattern ((proj2 ?l)) ) :rewrite-rule) )) - - -(declare-fun isnil1 (list) Bool) -(assert (= (isnil1 nil1) true)) -(assert (= (isnil1 nil2) false)) -(assert (forall ((?e elt) (?l list)) - (! (= (isnil1 (cons ?e ?l)) false) :rewrite-rule) )) -(assert (forall ((?l list)) - (! (=> true (=> (isnil1 ?l) (= ?l nil1))) :rewrite-rule) )) - -(declare-fun isnil2 (list) Bool) -(assert (= (isnil2 nil1) false)) -(assert (= (isnil2 nil2) true)) -(assert (forall ((?e elt) (?l list)) - (! (= (isnil2 (cons ?e ?l)) false) :rewrite-rule) )) -(assert (forall ((?l list)) - (! (=> true (=> (isnil2 ?l) (= ?l nil2))) :rewrite-rule) )) - -;; distinct -(assert (forall ((?l list)) - (! (=> (isnil1 ?l) (and (not (isnil2 ?l)) (not (iscons ?l))) ) :rewrite-rule) )) - -(assert (forall ((?l list)) - (! (=> (isnil2 ?l) (and (not (isnil1 ?l)) (not (iscons ?l))) ) :rewrite-rule) )) - -(assert (forall ((?l list)) - (! (=> (iscons ?l) (and (not (isnil1 ?l)) (not (isnil2 ?l))) ) :rewrite-rule) )) - - -;;;;;;;;;;;;;;;;;;; -;; case-split -(assert (forall ((?l list)) - (! (! (=> true (or (isnil1 ?l) (isnil2 ?l) (iscons ?l))) :pattern ((proj1 ?l)) ) :rewrite-rule) )) -(assert (forall ((?l list)) - (! (! (=> true (or (isnil1 ?l) (isnil2 ?l) (iscons ?l))) :pattern ((proj2 ?l)) ) :rewrite-rule) )) - -;;;;;;;;;;;;;;;;;;; -;; finite case-split -(assert (forall ((?l list)) - (! (=> (not (iscons ?l)) (or (isnil1 ?l) (isnil2 ?l))) :rewrite-rule) )) - - - -;;;;; goal - -(declare-fun e () elt) -(declare-fun l1 () list) -(declare-fun l2 () list) - - -(assert (not (=> (iscons l1) (=> (= (proj2 l1) (proj2 l2)) (= l1 (cons (proj1 l2) (proj2 l2))))))) - -(check-sat) - -(exit) diff --git a/test/regress/regress1/rewriterules/length_gen.smt2 b/test/regress/regress1/rewriterules/length_gen.smt2 deleted file mode 100644 index df876ef08..000000000 --- a/test/regress/regress1/rewriterules/length_gen.smt2 +++ /dev/null @@ -1,35 +0,0 @@ -; COMMAND-LINE: --rewrite-rules -;; Same than length.smt2 but the nil case is not a rewrite rule -;; So here the rewrite rules have no guards length - -(set-logic AUFLIA) -(set-info :status unsat) - -;; don't use a datatypes for currently focusing in uf -(declare-sort list 0) - -(declare-fun cons (Int list) list) -(declare-fun nil () list) - - -;;define length -(declare-fun length (list) Int) - -(assert (= (length nil) 0)) - -(assert (forall ((?e Int) (?l list)) (! (= (length (cons ?e ?l)) (+ 1 (length ?l))) :rewrite-rule))) - -(declare-fun gen_cons (Int list) list) - -(assert (forall ((?n Int) (?l list)) (! (=> (= ?n 0) (= (gen_cons ?n ?l) ?l)) :rewrite-rule))) - -(assert (forall ((?n Int) (?l list)) (! (=> (> ?n 0) (= (gen_cons ?n ?l) - (gen_cons (- ?n 1) (cons 1 ?l)))) :rewrite-rule))) - -(declare-fun n () Int) - -(assert (not (= (length (gen_cons 42 nil)) 42))) - -(check-sat) - -(exit) diff --git a/test/regress/regress1/rewriterules/length_gen_010.smt2 b/test/regress/regress1/rewriterules/length_gen_010.smt2 deleted file mode 100644 index aee09cc96..000000000 --- a/test/regress/regress1/rewriterules/length_gen_010.smt2 +++ /dev/null @@ -1,37 +0,0 @@ -; COMMAND-LINE: --rewrite-rules -;; Same than length.smt2 but the nil case is not a rewrite rule -;; So here the rewrite rules have no guards length - -(set-logic AUFLIA) -(set-info :status unsat) - -;; don't use a datatypes for currently focusing in uf -(declare-sort list 0) - -(declare-fun cons (Int list) list) -(declare-fun nil () list) - - -;;define length -(declare-fun length (list) Int) - -(assert (= (length nil) 0)) - -;; (assert (forall ((?e Int) (?l list)) (! (= (length (cons ?e ?l)) (+ 1 (length ?l))) :rewrite-rule))) - -(assert-rewrite ((?e Int) (?l list)) () () (length (cons ?e ?l)) (+ 1 (length ?l))) - -(declare-fun gen_cons (Int list) list) - -(assert-rewrite ((?n Int) (?l list)) () (= ?n 0) (gen_cons ?n ?l) (?l)) - -(assert-rewrite ((?n Int) (?l list)) () (> ?n 0) (gen_cons ?n ?l) - (gen_cons (- ?n 1) (cons 1 ?l))) - -(declare-fun n () Int) - -(assert (not (= (length (gen_cons 10 nil)) 10))) - -(check-sat) - -(exit) diff --git a/test/regress/regress1/rewriterules/length_gen_010_lemma.smt2 b/test/regress/regress1/rewriterules/length_gen_010_lemma.smt2 deleted file mode 100644 index 49e6f970d..000000000 --- a/test/regress/regress1/rewriterules/length_gen_010_lemma.smt2 +++ /dev/null @@ -1,35 +0,0 @@ -; COMMAND-LINE: --rewrite-rules -;; Same than length.smt2 but the nil case is not a rewrite rule -;; So here the rewrite rules have no guards length - -(set-logic AUFLIA) -(set-info :status unsat) - -;; don't use a datatypes for currently focusing in uf -(declare-sort list 0) - -(declare-fun cons (Int list) list) -(declare-fun nil () list) - - -;;define length -(declare-fun length (list) Int) - -(assert (= (length nil) 0)) - -(assert (forall ((?e Int) (?l list)) (= (length (cons ?e ?l)) (+ 1 (length ?l))))) - -(declare-fun gen_cons (Int list) list) - -(assert (forall ((?n Int) (?l list)) (=> (= ?n 0) (= (gen_cons ?n ?l) ?l)))) - -(assert (forall ((?n Int) (?l list)) (=> (> ?n 0) (= (gen_cons ?n ?l) - (gen_cons (- ?n 1) (cons 1 ?l)))))) - -(declare-fun n () Int) - -(assert (not (= (length (gen_cons 10 nil)) 10))) - -(check-sat) - -(exit) diff --git a/test/regress/regress1/rewriterules/length_gen_020.smt2 b/test/regress/regress1/rewriterules/length_gen_020.smt2 deleted file mode 100644 index b7c2e5fd2..000000000 --- a/test/regress/regress1/rewriterules/length_gen_020.smt2 +++ /dev/null @@ -1,35 +0,0 @@ -; COMMAND-LINE: --rewrite-rules -;; Same than length.smt2 but the nil case is not a rewrite rule -;; So here the rewrite rules have no guards length - -(set-logic AUFLIA) -(set-info :status unsat) - -;; don't use a datatypes for currently focusing in uf -(declare-sort list 0) - -(declare-fun cons (Int list) list) -(declare-fun nil () list) - - -;;define length -(declare-fun length (list) Int) - -(assert (= (length nil) 0)) - -(assert (forall ((?e Int) (?l list)) (! (= (length (cons ?e ?l)) (+ 1 (length ?l))) :rewrite-rule))) - -(declare-fun gen_cons (Int list) list) - -(assert (forall ((?n Int) (?l list)) (! (=> (= ?n 0) (= (gen_cons ?n ?l) ?l)) :rewrite-rule))) - -(assert (forall ((?n Int) (?l list)) (! (=> (> ?n 0) (= (gen_cons ?n ?l) - (gen_cons (- ?n 1) (cons 1 ?l)))) :rewrite-rule))) - -(declare-fun n () Int) - -(assert (not (= (length (gen_cons 20 nil)) 20))) - -(check-sat) - -(exit) diff --git a/test/regress/regress1/rewriterules/length_gen_020_sat.smt2 b/test/regress/regress1/rewriterules/length_gen_020_sat.smt2 deleted file mode 100644 index 72db8d18b..000000000 --- a/test/regress/regress1/rewriterules/length_gen_020_sat.smt2 +++ /dev/null @@ -1,35 +0,0 @@ -; COMMAND-LINE: --rewrite-rules --no-check-models -;; Same than length.smt2 but the nil case is not a rewrite rule -;; So here the rewrite rules have no guards length - -(set-logic AUFLIA) -(set-info :status sat) - -;; don't use a datatypes for currently focusing in uf -(declare-sort list 0) - -(declare-fun cons (Int list) list) -(declare-fun nil () list) - - -;;define length -(declare-fun length (list) Int) - -(assert (= (length nil) 0)) - -(assert (forall ((?e Int) (?l list)) (! (= (length (cons ?e ?l)) (+ 1 (length ?l))) :rewrite-rule))) - -(declare-fun gen_cons (Int list) list) - -(assert (forall ((?n Int) (?l list)) (! (=> (= ?n 0) (= (gen_cons ?n ?l) ?l)) :rewrite-rule))) - -(assert (forall ((?n Int) (?l list)) (! (=> (> ?n 0) (= (gen_cons ?n ?l) - (gen_cons (- ?n 1) (cons 1 ?l)))) :rewrite-rule))) - -(declare-fun n () Int) - -(assert (not (= (length (gen_cons 20 nil)) 200))) - -(check-sat) - -(exit) diff --git a/test/regress/regress1/rewriterules/length_gen_040.smt2 b/test/regress/regress1/rewriterules/length_gen_040.smt2 deleted file mode 100644 index 93a04cb7c..000000000 --- a/test/regress/regress1/rewriterules/length_gen_040.smt2 +++ /dev/null @@ -1,35 +0,0 @@ -; COMMAND-LINE: --rewrite-rules -;; Same than length.smt2 but the nil case is not a rewrite rule -;; So here the rewrite rules have no guards length - -(set-logic AUFLIA) -(set-info :status unsat) - -;; don't use a datatypes for currently focusing in uf -(declare-sort list 0) - -(declare-fun cons (Int list) list) -(declare-fun nil () list) - - -;;define length -(declare-fun length (list) Int) - -(assert (= (length nil) 0)) - -(assert (forall ((?e Int) (?l list)) (! (= (length (cons ?e ?l)) (+ 1 (length ?l))) :rewrite-rule))) - -(declare-fun gen_cons (Int list) list) - -(assert (forall ((?n Int) (?l list)) (! (=> (= ?n 0) (= (gen_cons ?n ?l) ?l)) :rewrite-rule))) - -(assert (forall ((?n Int) (?l list)) (! (=> (> ?n 0) (= (gen_cons ?n ?l) - (gen_cons (- ?n 1) (cons 1 ?l)))) :rewrite-rule))) - -(declare-fun n () Int) - -(assert (not (= (length (gen_cons 40 nil)) 40))) - -(check-sat) - -(exit) diff --git a/test/regress/regress1/rewriterules/length_gen_040_lemma.smt2 b/test/regress/regress1/rewriterules/length_gen_040_lemma.smt2 deleted file mode 100644 index cabd84575..000000000 --- a/test/regress/regress1/rewriterules/length_gen_040_lemma.smt2 +++ /dev/null @@ -1,35 +0,0 @@ -; COMMAND-LINE: --rewrite-rules -;; Same than length.smt2 but the nil case is not a rewrite rule -;; So here the rewrite rules have no guards length - -(set-logic AUFLIA) -(set-info :status unsat) - -;; don't use a datatypes for currently focusing in uf -(declare-sort list 0) - -(declare-fun cons (Int list) list) -(declare-fun nil () list) - - -;;define length -(declare-fun length (list) Int) - -(assert (= (length nil) 0)) - -(assert (forall ((?e Int) (?l list)) (= (length (cons ?e ?l)) (+ 1 (length ?l))))) - -(declare-fun gen_cons (Int list) list) - -(assert (forall ((?n Int) (?l list)) (=> (= ?n 0) (= (gen_cons ?n ?l) ?l)))) - -(assert (forall ((?n Int) (?l list)) (=> (> ?n 0) (= (gen_cons ?n ?l) - (gen_cons (- ?n 1) (cons 1 ?l)))))) - -(declare-fun n () Int) - -(assert (not (= (length (gen_cons 40 nil)) 40))) - -(check-sat) - -(exit) diff --git a/test/regress/regress1/rewriterules/length_gen_040_lemma_trigger.smt2 b/test/regress/regress1/rewriterules/length_gen_040_lemma_trigger.smt2 deleted file mode 100644 index 7530269e8..000000000 --- a/test/regress/regress1/rewriterules/length_gen_040_lemma_trigger.smt2 +++ /dev/null @@ -1,36 +0,0 @@ -; COMMAND-LINE: --rewrite-rules -;; Same than length.smt2 but the nil case is not a rewrite rule -;; So here the rewrite rules have no guards length - -(set-logic AUFLIA) -(set-info :status unsat) - -;; don't use a datatypes for currently focusing in uf -(declare-sort list 0) - -(declare-fun cons (Int list) list) -(declare-fun nil () list) - - -;;define length -(declare-fun length (list) Int) - -(assert (= (length nil) 0)) - -(assert (forall ((?e Int) (?l list)) (!(= (length (cons ?e ?l)) (+ 1 (length ?l))) :pattern ((length (cons ?e ?l))) ))) - -(declare-fun gen_cons (Int list) list) - -(assert (forall ((?n Int) (?l list)) (! (=> (= ?n 0) (= (gen_cons ?n ?l) ?l)) :pattern ((gen_cons ?n ?l)) ))) - -(assert (forall ((?n Int) (?l list)) (! (=> (> ?n 0) (= (gen_cons ?n ?l) - (gen_cons (- ?n 1) (cons 1 ?l)))) - :pattern ((gen_cons ?n ?l)) ))) - -(declare-fun n () Int) - -(assert (not (= (length (gen_cons 40 nil)) 40))) - -(check-sat) - -(exit) diff --git a/test/regress/regress1/rewriterules/length_gen_080.smt2 b/test/regress/regress1/rewriterules/length_gen_080.smt2 deleted file mode 100644 index 451ea091e..000000000 --- a/test/regress/regress1/rewriterules/length_gen_080.smt2 +++ /dev/null @@ -1,35 +0,0 @@ -; COMMAND-LINE: --rewrite-rules -;; Same than length.smt2 but the nil case is not a rewrite rule -;; So here the rewrite rules have no guards length - -(set-logic AUFLIA) -(set-info :status unsat) - -;; don't use a datatypes for currently focusing in uf -(declare-sort list 0) - -(declare-fun cons (Int list) list) -(declare-fun nil () list) - - -;;define length -(declare-fun length (list) Int) - -(assert (= (length nil) 0)) - -(assert (forall ((?e Int) (?l list)) (! (= (length (cons ?e ?l)) (+ 1 (length ?l))) :rewrite-rule))) - -(declare-fun gen_cons (Int list) list) - -(assert (forall ((?n Int) (?l list)) (! (=> (= ?n 0) (= (gen_cons ?n ?l) ?l)) :rewrite-rule))) - -(assert (forall ((?n Int) (?l list)) (! (=> (> ?n 0) (= (gen_cons ?n ?l) - (gen_cons (- ?n 1) (cons 1 ?l)))) :rewrite-rule))) - -(declare-fun n () Int) - -(assert (not (= (length (gen_cons 80 nil)) 80))) - -(check-sat) - -(exit) diff --git a/test/regress/regress1/rewriterules/length_gen_160_lemma.smt2 b/test/regress/regress1/rewriterules/length_gen_160_lemma.smt2 deleted file mode 100644 index 7a81652ea..000000000 --- a/test/regress/regress1/rewriterules/length_gen_160_lemma.smt2 +++ /dev/null @@ -1,35 +0,0 @@ -; COMMAND-LINE: --rewrite-rules -;; Same than length.smt2 but the nil case is not a rewrite rule -;; So here the rewrite rules have no guards length - -(set-logic AUFLIA) -(set-info :status unsat) - -;; don't use a datatypes for currently focusing in uf -(declare-sort list 0) - -(declare-fun cons (Int list) list) -(declare-fun nil () list) - - -;;define length -(declare-fun length (list) Int) - -(assert (= (length nil) 0)) - -(assert (forall ((?e Int) (?l list)) (= (length (cons ?e ?l)) (+ 1 (length ?l))))) - -(declare-fun gen_cons (Int list) list) - -(assert (forall ((?n Int) (?l list)) (=> (= ?n 0) (= (gen_cons ?n ?l) ?l)))) - -(assert (forall ((?n Int) (?l list)) (=> (> ?n 0) (= (gen_cons ?n ?l) - (gen_cons (- ?n 1) (cons 1 ?l)))))) - -(declare-fun n () Int) - -(assert (not (= (length (gen_cons 160 nil)) 160))) - -(check-sat) - -(exit) diff --git a/test/regress/regress1/rewriterules/length_gen_inv_160.smt2 b/test/regress/regress1/rewriterules/length_gen_inv_160.smt2 deleted file mode 100644 index af134287d..000000000 --- a/test/regress/regress1/rewriterules/length_gen_inv_160.smt2 +++ /dev/null @@ -1,35 +0,0 @@ -; COMMAND-LINE: --rewrite-rules -;; Same than length.smt2 but the nil case is not a rewrite rule -;; So here the rewrite rules have no guards length - -(set-logic AUFLIA) -(set-info :status unsat) - -;; don't use a datatypes for currently focusing in uf -(declare-sort list 0) - -(declare-fun cons (Int list) list) -(declare-fun nil () list) - - -;;define length -(declare-fun length (list) Int) - -(assert (= (length nil) 0)) - -(assert (forall ((?e Int) (?l list)) (! (= (length (cons ?e ?l)) (+ 1 (length ?l))) :rewrite-rule))) - -(declare-fun gen_cons (Int list) list) - -(assert (forall ((?n Int) (?l list)) (! (=> (= ?n 0) (= (gen_cons ?n ?l) ?l)) :rewrite-rule))) - -(assert (forall ((?n Int) (?l list)) (! (=> (> ?n 0) (= (gen_cons ?n ?l) - (cons 1 (gen_cons (- ?n 1) ?l)))) :rewrite-rule))) - -(declare-fun n () Int) - -(assert (not (= (length (gen_cons 160 nil)) 160))) - -(check-sat) - -(exit) diff --git a/test/regress/regress1/rewriterules/length_trick3.smt2 b/test/regress/regress1/rewriterules/length_trick3.smt2 deleted file mode 100644 index fce35d691..000000000 --- a/test/regress/regress1/rewriterules/length_trick3.smt2 +++ /dev/null @@ -1,37 +0,0 @@ -; COMMAND-LINE: --rewrite-rules -;; Same than length.smt2 but the nil case is not a rewrite rule -;; So here the rewrite rules have no guards length - -(set-logic AUFLIA) -(set-info :status unsat) - -;; don't use a datatypes for currently focusing in uf -(declare-sort list 0) -;; don't use arith -(declare-sort mynat 0) -(declare-fun zero () mynat) -(declare-fun succ (mynat) mynat) - -(declare-fun cons (Int list) list) -(declare-fun nil () list) - - -;;define length -(declare-fun length (list) mynat) - -(assert (= (length nil) zero)) - -(assert (forall ((?e Int) (?l list)) (! (= (length (cons ?e ?l)) (succ (length ?l))) :rewrite-rule))) - -(declare-fun ten_one_cons (list) list) - -(assert (forall ((?l list)) (! (= (ten_one_cons ?l) - (cons 1 (cons 1 (cons 1 (cons 1 (cons 1 (cons 1 (cons 1 (cons 1 (cons 1 (cons 1 ?l) ))))))))) - ) :rewrite-rule))) - -(assert (not (= (length (ten_one_cons nil)) - (succ(succ(succ(succ(succ(succ(succ(succ(succ(succ zero))))))))))))) - -(check-sat) - -(exit) diff --git a/test/regress/regress1/rewriterules/length_trick3_int.smt2 b/test/regress/regress1/rewriterules/length_trick3_int.smt2 deleted file mode 100644 index ec10ed6d3..000000000 --- a/test/regress/regress1/rewriterules/length_trick3_int.smt2 +++ /dev/null @@ -1,45 +0,0 @@ -; COMMAND-LINE: --rewrite-rules -;; Same than length.smt2 but the nil case is not a rewrite rule -;; So here the rewrite rules have no guards length - -(set-logic AUFLIA) -(set-info :status unsat) - -;; don't use a datatypes for currently focusing in uf -(declare-sort list 0) - -(declare-fun cons (Int list) list) -(declare-fun nil () list) - - -;;define length -(declare-fun length (list) Int) - -(assert (= (length nil) 0)) - -(assert (forall ((?e Int) (?l list)) (! (= (length (cons ?e ?l)) (+ 1 (length ?l))) :rewrite-rule))) - -(declare-fun ten_one_cons (list) list) - -(assert (forall ((?l list)) (! (= (ten_one_cons ?l) - (cons 1 (cons 1 (cons 1 (cons 1 (cons 1 (cons 1 (cons 1 (cons 1 (cons 1 (cons 1 ?l) ))))))))) - ) :rewrite-rule))) - -(assert (not (= (length (ten_one_cons nil)) - 10))) - -(check-sat) - -(declare-fun ten_one_ten (list) list) - -(assert (forall ((?l list)) (! (= (ten_one_ten ?l) - (ten_one_cons (ten_one_cons (ten_one_cons (ten_one_cons (ten_one_cons (ten_one_cons (ten_one_cons (ten_one_cons (ten_one_cons (ten_one_cons ?l) ))))))))) - ) :rewrite-rule))) - -(declare-fun two_one_ten (list) list) - -(assert (forall ((?l list)) (! (= (two_one_ten ?l) - (ten_one_cons (ten_one_cons ?l)) - ) :rewrite-rule))) - -(exit) diff --git a/test/regress/regress1/rewriterules/reachability_back_to_the_future.smt2 b/test/regress/regress1/rewriterules/reachability_back_to_the_future.smt2 deleted file mode 100644 index b73f1b2a4..000000000 --- a/test/regress/regress1/rewriterules/reachability_back_to_the_future.smt2 +++ /dev/null @@ -1,55 +0,0 @@ -; COMMAND-LINE: --rewrite-rules -;; Back to the Future ... Shuvendu K.Lhiri, Shaz Qadeer -(set-logic AUFLIA) -(set-info :status unsat) - -(declare-sort elt 0) - -(declare-fun f (elt) elt) -(declare-fun Rf (elt elt elt) Bool) - -;;eq -(assert-propagation ((?x elt)) ((?x)) () () (or (= ?x ?x) (not (= ?x ?x))) ) -;; reflexive -(assert-propagation ((?x elt)) ((?x)) () () (Rf ?x ?x ?x) ) -;; step -(assert-propagation ((?x elt)) (((f ?x))) () () (Rf ?x (f ?x) (f ?x)) ) -;; reach -(assert-propagation ((?x1 elt)(?x2 elt)) (((f ?x1))) () ((Rf ?x1 ?x2 ?x2)) (or (= ?x1 ?x2) (Rf ?x1 (f ?x1) ?x2)) ) -;; cycle -(assert-propagation ((?x1 elt)(?x2 elt)) (((f ?x1))) ((= (f ?x1) ?x1)) ((Rf ?x1 ?x2 ?x2)) (= ?x1 ?x2) ) -;; sandwich -(assert-propagation ((?x1 elt)(?x2 elt)) () () ((Rf ?x1 ?x2 ?x1)) (= ?x1 ?x2) ) -;; order1 -(assert-propagation ((?x1 elt)(?x2 elt)(?x3 elt)) () () ((Rf ?x1 ?x2 ?x2)(Rf ?x1 ?x3 ?x3)) - (or (Rf ?x1 ?x2 ?x3) (Rf ?x1 ?x3 ?x2)) ) -;; order2 -(assert-propagation ((?x1 elt)(?x2 elt)(?x3 elt)) () () ((Rf ?x1 ?x2 ?x3)) - (and (Rf ?x1 ?x2 ?x2) (Rf ?x2 ?x3 ?x3)) ) -;; transitive1 -(assert-propagation ((?x1 elt)(?x2 elt)(?x3 elt)) () () ((Rf ?x1 ?x2 ?x2)(Rf ?x2 ?x3 ?x3)) - (Rf ?x1 ?x3 ?x3) ) -;; transitive2 -(assert-propagation ((?x0 elt)(?x1 elt)(?x2 elt)(?x3 elt)) () () ((Rf ?x0 ?x1 ?x2)(Rf ?x1 ?x3 ?x2)) - (and (Rf ?x0 ?x1 ?x3) (Rf ?x0 ?x3 ?x2)) ) -;;transitive3 -(assert-propagation ((?x0 elt)(?x1 elt)(?x2 elt)(?x3 elt)) () () ((Rf ?x0 ?x1 ?x2)(Rf ?x0 ?x3 ?x1)) - (and (Rf ?x0 ?x3 ?x2) (Rf ?x3 ?x1 ?x2)) ) - -(declare-fun e1 () elt) -(declare-fun e2 () elt) -(declare-fun e3 () elt) -(declare-fun e4 () elt) - - -;; (assert (=> (Rf e1 e2 e3) (Rf e1 (f e1) (f e1)) )) - -;; (assert (=> (Rf e1 e2 e3) (Rf e1 e3 e3) )) - -;; (assert (=> (Rf e1 e2 e3) (or (= e1 e3) (Rf e1 (f e1) e3)) )) - -(assert (not (=> (and (not (= e1 e2)) (Rf e1 e2 e3)) (Rf e1 (f e1) e3) ))) - - -(check-sat) -(exit) \ No newline at end of file diff --git a/test/regress/regress1/rewriterules/read5.smt2 b/test/regress/regress1/rewriterules/read5.smt2 deleted file mode 100644 index 0f92effcb..000000000 --- a/test/regress/regress1/rewriterules/read5.smt2 +++ /dev/null @@ -1,36 +0,0 @@ -; COMMAND-LINE: --rewrite-rules -(set-logic AUF) -(set-info :source | -Translated from old SVC processor verification benchmarks. Contact Clark -Barrett at barrett@cs.stanford.edu for more information. - -This benchmark was automatically translated into SMT-LIB format from -CVC format using CVC Lite -|) -(set-info :smt-lib-version 2.0) -(set-info :category "crafted") -(set-info :status unsat) -(declare-sort Index 0) -(declare-sort Element 0)(declare-sort Arr 0)(declare-fun aselect (Arr Index) Element)(declare-fun astore (Arr Index Element) Arr)(declare-fun k (Arr Arr) Index) -(declare-fun a () Index) -(declare-fun aaa () Index) -(declare-fun aa () Index) -(declare-fun S () Arr) -(declare-fun vvv () Element) -(declare-fun v () Element) -(declare-fun vv () Element) -(declare-fun bbb () Index) -(declare-fun www () Element) -(declare-fun bb () Index) -(declare-fun ww () Element) -(declare-fun b () Index) -(declare-fun w () Element) -(declare-fun SS () Arr) -(assert (let ((?v_3 (ite (= a aa) false true)) (?v_4 (ite (= aa aaa) false true)) (?v_1 (astore (astore (astore S a v) aa vv) aaa vvv)) (?v_0 (astore S aaa vvv)) (?v_2 (astore S aa vv))) (not (ite (ite (ite (ite (= a aaa) false true) (ite ?v_3 ?v_4 false) false) (ite (= (astore (astore ?v_0 a v) aa vv) ?v_1) (ite (= (astore (astore ?v_0 aa vv) a v) ?v_1) (ite (= (astore (astore ?v_2 a v) aaa vvv) ?v_1) (= (astore (astore ?v_2 aaa vvv) a v) ?v_1) false) false) false) true) (ite (ite (= ?v_1 (astore (astore (astore S bbb www) bb ww) b w)) (ite (ite ?v_3 (ite ?v_4 (ite (ite (= aa b) false true) (ite (ite (= aa bb) false true) (ite (= aa bbb) false true) false) false) false) false) (= (aselect S aa) vv) true) true) (ite (= S (astore SS a v)) (= S (astore SS a (aselect S a))) true) false) false)))) -; rewrite rule definition of arrays theory -(assert (forall ((?x Arr) (?i Index) (?j Index) (?e Element)) (! (=> (not (= ?i ?j)) (= (aselect (astore ?x ?i ?e) ?j) (aselect ?x ?j))) :rewrite-rule))) -(assert (forall ((?x Arr) (?i Index) (?e Element)) (! (=> true (= (aselect (astore ?x ?i ?e) ?i) ?e)) :rewrite-rule))) -(assert (forall ((?x Arr) (?y Arr)) (! (=> (not (= ?x ?y)) (not (= (aselect ?x (k ?x ?y)) (aselect ?y (k ?x ?y))))) :rewrite-rule))) -(assert (forall ((?x Arr) (?y Arr)) (! (! (=> true (or (= ?x ?y) (not (= ?x ?y)))) :pattern (?x)) :rewrite-rule))) -(assert (forall ((?x Arr) (?i Index) (?j Index) (?e Element)) (! (! (=> true (or (= ?i ?j) (not (= ?i ?j)))) :pattern ((aselect (astore ?x ?i ?e) ?j))) :rewrite-rule)))(check-sat) -(exit) diff --git a/test/regress/regress1/rewriterules/set_A_new_fast_tableau-base.smt2 b/test/regress/regress1/rewriterules/set_A_new_fast_tableau-base.smt2 deleted file mode 100644 index 7434f4257..000000000 --- a/test/regress/regress1/rewriterules/set_A_new_fast_tableau-base.smt2 +++ /dev/null @@ -1,127 +0,0 @@ -; COMMAND-LINE: --rewrite-rules -;; A new fast tableau-base ... Domenico Cantone et Calogero G.Zarba -(set-logic AUFLIA) -(set-info :status unsat) - -;; don't use a datatypes for currently focusing in uf -(declare-sort elt 0) -(declare-sort set 0) - -(declare-fun in (elt set) Bool) - -;;;;;;;;;;;;;;;;;;;; -;; inter - -(declare-fun inter (set set) set) -(assert-propagation ((?s elt) (?t1 set) (?t2 set)) () () - ((in ?s (inter ?t1 ?t2))) (and (in ?s ?t1) (in ?s ?t2))) - - -(assert-propagation ((?s elt) (?t1 set) (?t2 set)) - (((inter ?t1 ?t2))) () ((not (in ?s ?t1))) (not (in ?s (inter ?t1 ?t2))) ) - -(assert-propagation ((?s elt) (?t1 set) (?t2 set)) - (((inter ?t1 ?t2))) () ((not (in ?s ?t2))) (not (in ?s (inter ?t1 ?t2))) ) - -(assert-propagation ((?s elt) (?t1 set) (?t2 set)) - () () ((not (in ?s (inter ?t1 ?t2))) (in ?s ?t1)) (not (in ?s ?t2)) ) - -(assert-propagation ((?s elt) (?t1 set) (?t2 set)) - () () ((not (in ?s (inter ?t1 ?t2))) (in ?s ?t2)) (not (in ?s ?t1))) - -(assert-propagation ((?s elt) (?t1 set) (?t2 set)) - (((inter ?t1 ?t2))) () ((in ?s ?t1) (in ?s ?t2)) (in ?s (inter ?t1 ?t2)) ) - -;;;;;;;;;;;;;;;;; -;; union - -(declare-fun union (set set) set) -(assert-propagation ((?s elt) (?t1 set) (?t2 set)) - () () ((not (in ?s (union ?t1 ?t2)))) (and (not (in ?s ?t1)) (not (in ?s ?t2)))) - -(assert-propagation ((?s elt) (?t1 set) (?t2 set)) - (((union ?t1 ?t2))) () ((in ?s ?t1)) (in ?s (union ?t1 ?t2))) - -(assert-propagation ((?s elt) (?t1 set) (?t2 set)) - (((union ?t1 ?t2))) () ((in ?s ?t2)) (in ?s (union ?t1 ?t2))) - -(assert-propagation ((?s elt) (?t1 set) (?t2 set)) - () () ((in ?s (union ?t1 ?t2)) (not (in ?s ?t1))) (in ?s ?t2)) - -(assert-propagation ((?s elt) (?t1 set) (?t2 set)) - () () ((in ?s (union ?t1 ?t2)) (not (in ?s ?t2))) (in ?s ?t1)) - -(assert-propagation ((?s elt) (?t1 set) (?t2 set)) - (((union ?t1 ?t2))) () ((not (in ?s ?t1)) (not (in ?s ?t2))) (not (in ?s (union ?t1 ?t2)))) - -;;;;;;;;;;;;;;;;;;;; -;; diff - -(declare-fun diff (set set) set) -(assert-propagation ((?s elt) (?t1 set) (?t2 set)) - () () ((in ?s (diff ?t1 ?t2))) (and (in ?s ?t1) (not (in ?s ?t2)))) - -(assert-propagation ((?s elt) (?t1 set) (?t2 set)) - (((diff ?t1 ?t2))) () ((not (in ?s ?t1))) (not (in ?s (diff ?t1 ?t2))) ) - -(assert-propagation ((?s elt) (?t1 set) (?t2 set)) - (((diff ?t1 ?t2))) () ((in ?s ?t2)) (not (in ?s (diff ?t1 ?t2)))) - -(assert-propagation ((?s elt) (?t1 set) (?t2 set)) - () () ((not (in ?s (diff ?t1 ?t2))) (in ?s ?t1)) (in ?s ?t2)) - -(assert-propagation ((?s elt) (?t1 set) (?t2 set)) - () () ((not (in ?s (diff ?t1 ?t2))) (not (in ?s ?t2))) (not (in ?s ?t1))) - -(assert-propagation ((?s elt) (?t1 set) (?t2 set)) - (((diff ?t1 ?t2))) () ((in ?s ?t1) (not (in ?s ?t2))) (in ?s (diff ?t1 ?t2)) ) - -;;;;;;;;;;;;;;;; -;;sing - -(declare-fun sing (elt) set) -(assert-propagation ((?s elt)) - (((sing ?s))) () () (in ?s (sing ?s)) ) - -(assert-propagation ((?s elt) (?t1 elt)) - () () ((in ?s (sing ?t1))) (= ?s ?t1)) - -(assert-propagation ((?s elt) (?t1 elt)) - () () ((not (in ?s (sing ?t1)))) (not (= ?s ?t1))) - -;;;;;;;;;;;;;;;;;;; -;; fullfiling runned at Full effort -(assert-propagation ((?s elt) (?t1 set) (?t2 set)) - () () ((in ?s (union ?t1 ?t2))) (or (in ?s ?t1) (not (in ?s ?t1)))) - -(assert-propagation ((?s elt) (?t1 set) (?t2 set)) - (((inter ?t1 ?t2))) () ((in ?s ?t1)) (or (in ?s ?t2) (not (in ?s ?t2)))) - -(assert-propagation ((?t1 set) (?t2 set)) - () () ((not (= ?t1 ?t2))) (exists ((?e elt)) (or (and (in ?e ?t1) (not (in ?e ?t2))) (and (not (in ?e ?t1)) (in ?e ?t2))))) - -;;;;;;;;;;;;;;;;;;; -;; shortcut -(declare-fun subset (set set) Bool) -(assert-reduction ((?t1 set) (?t2 set)) - () () ((subset ?t1 ?t2)) (= (union ?t1 ?t2) ?t2)) - -(declare-fun e () elt) -(declare-fun t1 () set) -(declare-fun t2 () set) -(declare-fun t3 () set) - -;;(assert (not (=> (in e (inter (union t1 t2) (union t1 t1))) (in e (union t1 t1))))) -;;(assert (not (=> (in e (union t1 t1)) (in e t1)))) - -;; hyp -;;(assert (=> (in e (union t1 t1)) (in e t1))) - -;;(assert (not (=> (in e (inter (union t1 t2) (union t1 t1))) (in e t1)))) - -;;(assert (or (and (not (in e (union t1 (union t2 t3)))) (in e (union (union t1 t2) t3))) (and (in e (union t1 (union t2 t3))) (not (in e (union (union t1 t2) t3))))) ) -(assert (not (= (union t1 (union t2 t3)) (union (union t1 t2) t3))) ) - -(check-sat) - -(exit) diff --git a/test/regress/regress1/rewriterules/set_A_new_fast_tableau-base_sat.smt2 b/test/regress/regress1/rewriterules/set_A_new_fast_tableau-base_sat.smt2 deleted file mode 100644 index 256c9bb11..000000000 --- a/test/regress/regress1/rewriterules/set_A_new_fast_tableau-base_sat.smt2 +++ /dev/null @@ -1,128 +0,0 @@ -; COMMAND-LINE: --rewrite-rules -;; A new fast tableau-base ... Domenico Cantone et Calogero G.Zarba -(set-logic AUFLIA) -(set-info :status sat) - -;; don't use a datatypes for currently focusing in uf -(declare-sort elt 0) -(declare-sort set 0) - -(declare-fun in (elt set) Bool) - - -;;;;;;;;;;;;;;;;;;;; -;; inter - -(declare-fun inter (set set) set) -(assert-propagation ((?s elt) (?t1 set) (?t2 set)) () () - ((in ?s (inter ?t1 ?t2))) (and (in ?s ?t1) (in ?s ?t2))) - - -(assert-propagation ((?s elt) (?t1 set) (?t2 set)) - (((inter ?t1 ?t2))) () ((not (in ?s ?t1))) (not (in ?s (inter ?t1 ?t2))) ) - -(assert-propagation ((?s elt) (?t1 set) (?t2 set)) - (((inter ?t1 ?t2))) () ((not (in ?s ?t2))) (not (in ?s (inter ?t1 ?t2))) ) - -(assert-propagation ((?s elt) (?t1 set) (?t2 set)) - () () ((not (in ?s (inter ?t1 ?t2))) (in ?s ?t1)) (not (in ?s ?t2)) ) - -(assert-propagation ((?s elt) (?t1 set) (?t2 set)) - () () ((not (in ?s (inter ?t1 ?t2))) (in ?s ?t2)) (not (in ?s ?t1))) - -(assert-propagation ((?s elt) (?t1 set) (?t2 set)) - (((inter ?t1 ?t2))) () ((in ?s ?t1) (in ?s ?t2)) (in ?s (inter ?t1 ?t2)) ) - -;;;;;;;;;;;;;;;;; -;; union - -(declare-fun union (set set) set) -(assert-propagation ((?s elt) (?t1 set) (?t2 set)) - () () ((not (in ?s (union ?t1 ?t2)))) (and (not (in ?s ?t1)) (not (in ?s ?t2)))) - -(assert-propagation ((?s elt) (?t1 set) (?t2 set)) - (((union ?t1 ?t2))) () ((in ?s ?t1)) (in ?s (union ?t1 ?t2))) - -(assert-propagation ((?s elt) (?t1 set) (?t2 set)) - (((union ?t1 ?t2))) () ((in ?s ?t2)) (in ?s (union ?t1 ?t2))) - -(assert-propagation ((?s elt) (?t1 set) (?t2 set)) - () () ((in ?s (union ?t1 ?t2)) (not (in ?s ?t1))) (in ?s ?t2)) - -(assert-propagation ((?s elt) (?t1 set) (?t2 set)) - () () ((in ?s (union ?t1 ?t2)) (not (in ?s ?t2))) (in ?s ?t1)) - -(assert-propagation ((?s elt) (?t1 set) (?t2 set)) - (((union ?t1 ?t2))) () ((not (in ?s ?t1)) (not (in ?s ?t2))) (not (in ?s (union ?t1 ?t2)))) - -;;;;;;;;;;;;;;;;;;;; -;; diff - -(declare-fun diff (set set) set) -(assert-propagation ((?s elt) (?t1 set) (?t2 set)) - () () ((in ?s (diff ?t1 ?t2))) (and (in ?s ?t1) (not (in ?s ?t2)))) - -(assert-propagation ((?s elt) (?t1 set) (?t2 set)) - (((diff ?t1 ?t2))) () ((not (in ?s ?t1))) (not (in ?s (diff ?t1 ?t2))) ) - -(assert-propagation ((?s elt) (?t1 set) (?t2 set)) - (((diff ?t1 ?t2))) () ((in ?s ?t2)) (not (in ?s (diff ?t1 ?t2)))) - -(assert-propagation ((?s elt) (?t1 set) (?t2 set)) - () () ((not (in ?s (diff ?t1 ?t2))) (in ?s ?t1)) (in ?s ?t2)) - -(assert-propagation ((?s elt) (?t1 set) (?t2 set)) - () () ((not (in ?s (diff ?t1 ?t2))) (not (in ?s ?t2))) (not (in ?s ?t1))) - -(assert-propagation ((?s elt) (?t1 set) (?t2 set)) - (((diff ?t1 ?t2))) () ((in ?s ?t1) (not (in ?s ?t2))) (in ?s (diff ?t1 ?t2)) ) - -;;;;;;;;;;;;;;;; -;;sing - -(declare-fun sing (elt) set) -(assert-propagation ((?s elt)) - (((sing ?s))) () () (in ?s (sing ?s)) ) - -(assert-propagation ((?s elt) (?t1 elt)) - () () ((in ?s (sing ?t1))) (= ?s ?t1)) - -(assert-propagation ((?s elt) (?t1 elt)) - () () ((not (in ?s (sing ?t1)))) (not (= ?s ?t1))) - -;;;;;;;;;;;;;;;;;;; -;; fullfiling runned at Full effort -(assert-propagation ((?s elt) (?t1 set) (?t2 set)) - () () ((in ?s (union ?t1 ?t2))) (or (in ?s ?t1) (not (in ?s ?t1)))) - -(assert-propagation ((?s elt) (?t1 set) (?t2 set)) - (((inter ?t1 ?t2))) () ((in ?s ?t1)) (or (in ?s ?t2) (not (in ?s ?t2)))) - -(assert-propagation ((?t1 set) (?t2 set)) - () () ((not (= ?t1 ?t2))) (exists ((?e elt)) (or (and (in ?e ?t1) (not (in ?e ?t2))) (and (not (in ?e ?t1)) (in ?e ?t2))))) - -;;;;;;;;;;;;;;;;;;; -;; shortcut -(declare-fun subset (set set) Bool) -(assert-reduction ((?t1 set) (?t2 set)) - () () ((subset ?t1 ?t2)) (= (union ?t1 ?t2) ?t2)) - -(declare-fun e () elt) -(declare-fun t1 () set) -(declare-fun t2 () set) -(declare-fun t3 () set) - -;;(assert (not (=> (in e (inter (union t1 t2) (union t1 t1))) (in e (union t1 t1))))) -;;(assert (not (=> (in e (union t1 t1)) (in e t1)))) - -;; hyp -;;(assert (=> (in e (union t1 t1)) (in e t1))) - -;;(assert (not (=> (in e (inter (union t1 t2) (union t1 t1))) (in e t1)))) - -(assert (or (and (not (in e (union t1 (union t2 t3)))) (in e (union (union t1 t2) t3))) (and (in e (union t1 (union t2 t3))) (not (in e (union (union t2 t2) t3))))) ) - - -(check-sat) - -(exit) diff --git a/test/regress/regress1/rewriterules/test_guards.smt2 b/test/regress/regress1/rewriterules/test_guards.smt2 deleted file mode 100644 index 7344dfba5..000000000 --- a/test/regress/regress1/rewriterules/test_guards.smt2 +++ /dev/null @@ -1,46 +0,0 @@ -; COMMAND-LINE: --rewrite-rules -;; Same than length.smt2 but the nil case is not a rewrite rule -;; So here the rewrite rules have no guards length - -(set-logic AUFLIA) -(set-info :status unsat) - -;; don't use a datatypes for currently focusing in uf -(declare-sort list 0) -;; don't use arith -(declare-sort mynat 0) -(declare-fun zero () mynat) -(declare-fun succ (mynat) mynat) - -(declare-fun cons (Int list) list) -(declare-fun nil () list) -(declare-fun p (list) Bool) - - -;;define length -(declare-fun length (list) mynat) - -(assert (= (length nil) zero)) - -(assert (forall ((?e Int) (?l list)) (! (= (length (cons ?e ?l)) (succ (length ?l))) :rewrite-rule))) - -(declare-fun ten_one_cons (list) list) - -(assert (forall ((?l list)) (! (=> (p ?l) (= (ten_one_cons ?l) - (cons 1 (cons 1 (cons 1 (cons 1 (cons 1 (cons 1 (cons 1 (cons 1 (cons 1 (cons 1 ?l) ))))))))) - )) :rewrite-rule))) - -(declare-fun a () Bool) -(declare-fun b () Bool) -(declare-fun c () Bool) - -(assert (=> a (p nil)) ) -(assert (=> b (p nil)) ) -(assert (or a b)) - -(assert (not (= (length (ten_one_cons nil)) - (succ(succ(succ(succ(succ(succ(succ(succ(succ(succ zero))))))))))))) - -(check-sat) - -(exit) diff --git a/test/regress/regress1/rewriterules/why3_vstte10_max_sum_harness2.smt2 b/test/regress/regress1/rewriterules/why3_vstte10_max_sum_harness2.smt2 deleted file mode 100644 index 5646cd70b..000000000 --- a/test/regress/regress1/rewriterules/why3_vstte10_max_sum_harness2.smt2 +++ /dev/null @@ -1,493 +0,0 @@ -; COMMAND-LINE: --rewrite-rules -;;; From a verification condition generated by why3. The original program -;; can be found at http://toccata.lri.fr/gallery/vstte10_max_sum.en.html . -;; The problem has been modified by doubling the size of the arrays -;; (* **) -;; VSTTE'10 competition http://www.macs.hw.ac.uk/vstte10/Competition.html **) -;; Problem 1: maximum /\ sum of an array **) - -;; Author: Jean-Christophe Filliatre (CNRS) **) -;; Tool: Why3 (see http://why3.lri.fr/) **) -;; *\) **) - -;; Particularly the assertion in the test case that the sum s = 90 - -;;; this is a prelude for CVC4 -(set-logic AUFNIRA) -;;; this is a prelude for CVC4 integer arithmetic -(declare-sort uni 0) - -(declare-sort deco 0) - -(declare-sort ty 0) - -(declare-fun sort (ty uni) deco) - -(declare-fun int () ty) - -(declare-fun real () ty) - -(declare-fun bool () ty) - -(declare-fun True () uni) - -(declare-fun False () uni) - -(declare-fun match_bool (deco deco deco) uni) - -;; match_bool_True - (assert - (forall ((a ty)) - (forall ((z uni) (z1 uni)) - (= (sort a (match_bool (sort bool True) (sort a z) (sort a z1))) (sort a z))))) - -;; match_bool_False - (assert - (forall ((a ty)) - (forall ((z uni) (z1 uni)) - (= (sort a (match_bool (sort bool False) (sort a z) (sort a z1))) (sort a - z1))))) - -(declare-fun index_bool (deco) Int) - -;; index_bool_True - (assert (= (index_bool (sort bool True)) 0)) - -;; index_bool_False - (assert (= (index_bool (sort bool False)) 1)) - -;; bool_inversion - (assert - (forall ((u uni)) - (or (= (sort bool u) (sort bool True)) (= (sort bool u) (sort bool False))))) - -(declare-fun tuple0 () ty) - -(declare-fun Tuple0 () uni) - -;; tuple0_inversion - (assert (forall ((u uni)) (= (sort tuple0 u) (sort tuple0 Tuple0)))) - -;; CompatOrderMult - (assert - (forall ((x Int) (y Int) (z Int)) - (=> (<= x y) (=> (<= 0 z) (<= (* x z) (* y z)))))) - -(declare-fun ref (ty) ty) - -(declare-fun mk_ref (deco) uni) - -(declare-fun contents (deco) uni) - -;; contents_def - (assert - (forall ((a ty)) - (forall ((u uni)) - (= (sort a (contents (sort (ref a) (mk_ref (sort a u))))) (sort a u))))) - -;; ref_inversion - (assert - (forall ((a ty)) - (forall ((u uni)) - (= (sort (ref a) u) (sort (ref a) - (mk_ref (sort a (contents (sort (ref a) u))))))))) - -(declare-fun map (ty ty) ty) - -(declare-fun get (deco deco) uni) - -(declare-fun set (deco deco deco) uni) - -;; Select_eq - (assert - (forall ((m (Array Int Int))) - (forall ((a1 Int) (a2 Int)) - (forall ((b Int)) - (! (=> (= a1 a2) (= (select (store m a1 b) a2) b)) :pattern ((select (store m a1 b) a2)) ))))) - -;; Select_eq - (assert - (forall ((a ty) (b ty)) - (forall ((m uni)) - (forall ((a1 uni) (a2 uni)) - (forall ((b1 uni)) - (! (=> (= (sort a a1) (sort a a2)) - (= (sort b - (get - (sort (map a b) (set (sort (map a b) m) (sort a a1) (sort b b1))) - (sort a a2))) (sort b b1))) :pattern ((sort b - (get - (sort (map a b) - (set (sort (map a b) m) - (sort a a1) (sort b b1))) - (sort a a2)))) )))))) - -;; Select_neq - (assert - (forall ((m (Array Int Int))) - (forall ((a1 Int) (a2 Int)) - (forall ((b Int)) - (! (=> (not (= a1 a2)) (= (select (store m a1 b) a2) (select m a2))) :pattern ((select (store m a1 b) a2)) ))))) - -;; Select_neq - (assert - (forall ((a ty) (b ty)) - (forall ((m uni)) - (forall ((a1 uni) (a2 uni)) - (forall ((b1 uni)) - (! (=> (not (= (sort a a1) (sort a a2))) - (= (sort b - (get - (sort (map a b) (set (sort (map a b) m) (sort a a1) (sort b b1))) - (sort a a2))) (sort b (get (sort (map a b) m) (sort a a2))))) :pattern ( - (sort b - (get (sort (map a b) (set (sort (map a b) m) (sort a a1) (sort b b1))) - (sort a a2)))) )))))) - -(declare-fun const1 (deco) uni) - -(declare-fun const2 (Int) (Array Int Int)) - -;; Const - (assert (forall ((b Int) (a Int)) (= (select (const2 b) a) b))) - -;; Const - (assert - (forall ((a ty) (b ty)) - (forall ((b1 uni) (a1 uni)) - (= (sort b (get (sort (map a b) (const1 (sort b b1))) (sort a a1))) - (sort b b1))))) - -(declare-sort array 1) - -(declare-fun array1 (ty) ty) - -(declare-fun mk_array (Int deco) uni) - -(declare-fun mk_array1 (Int (Array Int Int)) (array Int)) - -(declare-fun length (deco) Int) - -(declare-fun t2tb ((array Int)) uni) - -(declare-fun tb2t (deco) (array Int)) - -;; BridgeL - (assert - (forall ((i (array Int))) - (! (= (tb2t (sort (array1 int) (t2tb i))) i) :pattern ((sort (array1 int) - (t2tb i))) ))) - -;; BridgeR - (assert - (forall ((j uni)) - (! (= (sort (array1 int) (t2tb (tb2t (sort (array1 int) j)))) (sort - (array1 int) - j)) :pattern ( - (sort (array1 int) (t2tb (tb2t (sort (array1 int) j))))) ))) - -;; length_def - (assert - (forall ((u Int) (u1 (Array Int Int))) - (= (length (sort (array1 int) (t2tb (mk_array1 u u1)))) u))) - -;; length_def - (assert - (forall ((a ty)) - (forall ((u Int) (u1 uni)) - (= (length (sort (array1 a) (mk_array u (sort (map int a) u1)))) u)))) - -(declare-fun elts (deco) uni) - -(declare-fun t2tb1 ((Array Int Int)) uni) - -(declare-fun tb2t1 (deco) (Array Int Int)) - -;; BridgeL - (assert - (forall ((i (Array Int Int))) - (! (= (tb2t1 (sort (map int int) (t2tb1 i))) i) :pattern ((sort - (map int int) - (t2tb1 i))) ))) - -;; BridgeR - (assert - (forall ((j uni)) - (! (= (sort (map int int) (t2tb1 (tb2t1 (sort (map int int) j)))) (sort - (map - int - int) j)) :pattern ( - (sort (map int int) (t2tb1 (tb2t1 (sort (map int int) j))))) ))) - -;; elts_def - (assert - (forall ((u Int) (u1 (Array Int Int))) - (= (tb2t1 - (sort (map int int) (elts (sort (array1 int) (t2tb (mk_array1 u u1)))))) u1))) - -;; elts_def - (assert - (forall ((a ty)) - (forall ((u Int) (u1 uni)) - (= (sort (map int a) - (elts (sort (array1 a) (mk_array u (sort (map int a) u1))))) (sort - (map int a) - u1))))) - -;; array_inversion - (assert - (forall ((u (array Int))) - (= u (mk_array1 (length (sort (array1 int) (t2tb u))) - (tb2t1 (sort (map int int) (elts (sort (array1 int) (t2tb u))))))))) - -;; array_inversion - (assert - (forall ((a ty)) - (forall ((u uni)) - (= (sort (array1 a) u) (sort (array1 a) - (mk_array (length (sort (array1 a) u)) - (sort (map int a) (elts (sort (array1 a) u))))))))) - -(declare-fun get1 (deco Int) uni) - -(declare-fun t2tb2 (Int) uni) - -(declare-fun tb2t2 (deco) Int) - -;; BridgeL - (assert - (forall ((i Int)) - (! (= (tb2t2 (sort int (t2tb2 i))) i) :pattern ((sort int (t2tb2 i))) ))) - -;; BridgeR - (assert - (forall ((j uni)) - (! (= (sort int (t2tb2 (tb2t2 (sort int j)))) (sort int j)) :pattern ( - (sort int (t2tb2 (tb2t2 (sort int j))))) ))) - -;; get_def - (assert - (forall ((a (array Int)) (i Int)) - (= (tb2t2 (sort int (get1 (sort (array1 int) (t2tb a)) i))) (select - (tb2t1 (sort (map int int) (elts (sort (array1 int) (t2tb a))))) i)))) - -;; get_def - (assert - (forall ((a ty)) - (forall ((a1 uni) (i Int)) - (= (sort a (get1 (sort (array1 a) a1) i)) (sort a - (get - (sort (map int a) - (elts (sort (array1 a) a1))) - (sort int (t2tb2 i)))))))) - -(declare-fun set1 (deco Int deco) uni) - -;; set_def - (assert - (forall ((a (array Int)) (i Int) (v Int)) - (= (tb2t - (sort (array1 int) - (set1 (sort (array1 int) (t2tb a)) i (sort int (t2tb2 v))))) (mk_array1 - (length - (sort - (array1 - int) - (t2tb a))) - (store - (tb2t1 - (sort - (map - int - int) - (elts - (sort - (array1 - int) - (t2tb a))))) i v))))) - -;; set_def - (assert - (forall ((a ty)) - (forall ((a1 uni) (i Int) (v uni)) - (= (sort (array1 a) (set1 (sort (array1 a) a1) i (sort a v))) (sort - (array1 a) - (mk_array - (length - (sort - (array1 a) - a1)) - (sort - (map int a) - (set - (sort - (map int a) - (elts - (sort - (array1 a) - a1))) - (sort - int - (t2tb2 i)) - (sort a v))))))))) - -(declare-fun make (Int deco) uni) - -;; make_def - (assert - (forall ((n Int) (v Int)) - (= (tb2t (sort (array1 int) (make n (sort int (t2tb2 v))))) (mk_array1 n - (const2 v))))) - -;; make_def - (assert - (forall ((a ty)) - (forall ((n Int) (v uni)) - (= (sort (array1 a) (make n (sort a v))) (sort (array1 a) - (mk_array n - (sort (map int a) - (const1 (sort a v))))))))) - -(declare-fun sum ((Array Int Int) Int Int) Int) - -;; Sum_def_empty - (assert - (forall ((c (Array Int Int)) (i Int) (j Int)) - (=> (<= j i) (= (sum c i j) 0)))) - -;; Sum_def_non_empty - (assert - (forall ((c (Array Int Int)) (i Int) (j Int)) - (=> (< i j) (= (sum c i j) (+ (select c i) (sum c (+ i 1) j)))))) - -;; Sum_right_extension - (assert - (forall ((c (Array Int Int)) (i Int) (j Int)) - (=> (< i j) (= (sum c i j) (+ (sum c i (- j 1)) (select c (- j 1))))))) - -;; Sum_transitivity - (assert - (forall ((c (Array Int Int)) (i Int) (k Int) (j Int)) - (=> (and (<= i k) (<= k j)) (= (sum c i j) (+ (sum c i k) (sum c k j)))))) - -;; Sum_eq - (assert - (forall ((c1 (Array Int Int)) (c2 (Array Int Int)) (i Int) (j Int)) - (=> - (forall ((k Int)) - (=> (and (<= i k) (< k j)) (= (select c1 k) (select c2 k)))) - (= (sum c1 i j) (sum c2 i j))))) - -(declare-fun sum1 ((array Int) Int Int) Int) - -;; sum_def - (assert - (forall ((a (array Int)) (l Int) (h Int)) - (= (sum1 a l h) (sum - (tb2t1 - (sort (map int int) (elts (sort (array1 int) (t2tb a))))) l - h)))) - -(declare-fun is_max ((array Int) Int Int Int) Bool) - -;; is_max_def - (assert - (forall ((a (array Int)) (l Int) (h Int) (m Int)) - (and - (=> (is_max a l h m) - (and - (forall ((k Int)) - (=> (and (<= l k) (< k h)) - (<= (tb2t2 (sort int (get1 (sort (array1 int) (t2tb a)) k))) m))) - (or (and (<= h l) (= m 0)) - (and (< l h) - (exists ((k Int)) - (and (and (<= l k) (< k h)) - (= m (tb2t2 (sort int (get1 (sort (array1 int) (t2tb a)) k)))))))))) - (=> - (and - (forall ((k Int)) - (=> (and (<= l k) (< k h)) - (<= (tb2t2 (sort int (get1 (sort (array1 int) (t2tb a)) k))) m))) - (or (and (<= h l) (= m 0)) - (and (< l h) - (exists ((k Int)) - (and (and (<= l k) (< k h)) - (= m (tb2t2 (sort int (get1 (sort (array1 int) (t2tb a)) k))))))))) (is_max - a l h m))))) - -(assert -;; WP_parameter_test_case - ;; File "vstte10_max_sum/../vstte10_max_sum.mlw", line 63, characters 6-15 - (not - (=> (<= 0 20) - (=> (and (<= 0 0) (< 0 20)) - (forall ((a (Array Int Int))) - (=> (= a (store (const2 0) 0 9)) - (=> (and (<= 0 1) (< 1 20)) - (forall ((a1 (Array Int Int))) - (=> (= a1 (store a 1 5)) - (=> (and (<= 0 2) (< 2 20)) - (forall ((a2 (Array Int Int))) - (=> (= a2 (store a1 2 0)) - (=> (and (<= 0 3) (< 3 20)) - (forall ((a3 (Array Int Int))) - (=> (= a3 (store a2 3 2)) - (=> (and (<= 0 4) (< 4 20)) - (forall ((a4 (Array Int Int))) - (=> (= a4 (store a3 4 7)) - (=> (and (<= 0 5) (< 5 20)) - (forall ((a5 (Array Int Int))) - (=> (= a5 (store a4 5 3)) - (=> (and (<= 0 6) (< 6 20)) - (forall ((a6 (Array Int Int))) - (=> (= a6 (store a5 6 2)) - (=> (and (<= 0 7) (< 7 20)) - (forall ((a7 (Array Int Int))) - (=> (= a7 (store a6 7 1)) - (=> (and (<= 0 8) (< 8 20)) - (forall ((a8 (Array Int Int))) - (=> (= a8 (store a7 8 10)) - (=> (and (<= 0 9) (< 9 20)) - (forall ((a9 (Array Int Int))) - (=> (= a9 (store a8 9 6)) - (=> (and (<= 0 10) (< 10 20)) - (forall ((a10 (Array Int Int))) - (=> (= a10 (store a9 10 9)) - (=> (and (<= 0 11) (< 11 20)) - (forall ((a11 (Array Int Int))) - (=> (= a11 (store a10 11 5)) - (=> (and (<= 0 12) (< 12 20)) - (forall ((a12 (Array Int Int))) - (=> (= a12 (store a11 12 0)) - (=> (and (<= 0 13) (< 13 20)) - (forall ((a13 (Array Int Int))) - (=> (= a13 (store a12 13 2)) - (=> (and (<= 0 14) (< 14 20)) - (forall ((a14 (Array Int Int))) - (=> (= a14 (store a13 14 7)) - (=> (and (<= 0 15) (< 15 20)) - (forall ((a15 (Array Int Int))) - (=> (= a15 (store a14 15 3)) - (=> (and (<= 0 16) (< 16 20)) - (forall ((a16 (Array Int Int))) - (=> (= a16 (store a15 16 2)) - (=> (and (<= 0 17) (< 17 20)) - (forall ((a17 (Array Int Int))) - (=> (= a17 (store a16 17 1)) - (=> (and (<= 0 18) (< 18 20)) - (forall ((a18 (Array Int Int))) - (=> (= a18 (store a17 18 10)) - (=> (and (<= 0 19) (< 19 20)) - (forall ((a19 (Array Int Int))) - (=> (= a19 (store a18 19 6)) - (=> - (and (<= 0 20) - (forall ((i Int)) (=> (and (<= 0 i) (< i 20)) (<= 0 (select a19 i))))) - (forall ((result Int) (result1 Int)) - (=> - (and (= result (sum a19 0 20)) - (and (is_max (mk_array1 20 a19) 0 20 result1) (<= result (* 20 result1)))) - (= result 90))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) -(check-sat) - -- 2.30.2