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
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 ------------------------------------------------------------ */
${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
${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
### 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"
| 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(); }
}
;
-rewriterulesCommand[std::unique_ptr<CVC4::Command>* cmd]
-@declarations {
- std::vector<Expr> 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<Expr> patexpr;
| 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))); }
;
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); }
}
)+ 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<f2.getNumChildren(); i++ ){
if( f2[i].getKind()==kind::INST_PATTERN ){
BLOCK_MODEL_TOK : 'block-model';
BLOCK_MODEL_VALUES_TOK : 'block-model-values';
ECHO_TOK : 'echo';
-REWRITE_RULE_TOK : 'assert-rewrite';
-REDUCTION_RULE_TOK : 'assert-reduction';
-PROPAGATION_RULE_TOK : 'assert-propagation';
DECLARE_SORTS_TOK : 'declare-sorts';
DECLARE_FUNS_TOK : 'declare-funs';
DECLARE_PREDS_TOK : 'declare-preds';
}
}
-std::unique_ptr<Command> Smt2::assertRewriteRule(
- Kind kind,
- Expr bvl,
- const std::vector<Expr>& triggers,
- const std::vector<Expr>& guards,
- const std::vector<Expr>& heads,
- Expr body)
-{
- assert(kind == kind::RR_REWRITE || kind == kind::RR_REDUCTION
- || kind == kind::RR_DEDUCTION);
-
- ExprManager* em = getExprManager();
-
- std::vector<Expr> 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<Command>(new AssertCommand(rule, false));
-}
-
Smt2::SynthFunFactory::SynthFunFactory(
Smt2* smt2,
const std::string& fun,
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<Command> assertRewriteRule(Kind kind,
- Expr bvl,
- const std::vector<Expr>& triggers,
- const std::vector<Expr>& guards,
- const std::vector<Expr>& heads,
- Expr body);
-
/**
* Class for creating instances of `SynthFunCommand`s. Creating an instance
* of this class pushes the scope, destroying it pops the scope.
return "declare-datatypes";
}
-/* -------------------------------------------------------------------------- */
-/* class RewriteRuleCommand */
-/* -------------------------------------------------------------------------- */
-
-RewriteRuleCommand::RewriteRuleCommand(const std::vector<Expr>& vars,
- const std::vector<Expr>& 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<Expr>& vars,
- Expr head,
- Expr body)
- : d_vars(vars), d_head(head), d_body(body)
-{
-}
-
-const std::vector<Expr>& RewriteRuleCommand::getVars() const { return d_vars; }
-const std::vector<Expr>& 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<bool>(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<Expr> 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<Expr>& 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<Expr>& vars,
- const std::vector<Expr>& guards,
- const std::vector<Expr>& 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<Expr>& vars,
- const std::vector<Expr>& heads,
- Expr body,
- bool deduction)
- : d_vars(vars), d_heads(heads), d_body(body), d_deduction(deduction)
-{
-}
-
-const std::vector<Expr>& PropagateRuleCommand::getVars() const
-{
- return d_vars;
-}
-
-const std::vector<Expr>& PropagateRuleCommand::getGuards() const
-{
- return d_guards;
-}
-
-const std::vector<Expr>& 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<bool>(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<Expr> 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<Expr>& 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
std::string getCommandName() const override;
}; /* class DatatypeDeclarationCommand */
-class CVC4_PUBLIC RewriteRuleCommand : public Command
-{
- public:
- typedef std::vector<std::vector<Expr> > Triggers;
-
- protected:
- typedef std::vector<Expr> VExpr;
- VExpr d_vars;
- VExpr d_guards;
- Expr d_head;
- Expr d_body;
- Triggers d_triggers;
-
- public:
- RewriteRuleCommand(const std::vector<Expr>& vars,
- const std::vector<Expr>& guards,
- Expr head,
- Expr body,
- const Triggers& d_triggers);
- RewriteRuleCommand(const std::vector<Expr>& vars, Expr head, Expr body);
-
- const std::vector<Expr>& getVars() const;
- const std::vector<Expr>& 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<std::vector<Expr> > Triggers;
-
- protected:
- typedef std::vector<Expr> VExpr;
- VExpr d_vars;
- VExpr d_guards;
- VExpr d_heads;
- Expr d_body;
- Triggers d_triggers;
- bool d_deduction;
-
- public:
- PropagateRuleCommand(const std::vector<Expr>& vars,
- const std::vector<Expr>& guards,
- const std::vector<Expr>& heads,
- Expr body,
- const Triggers& d_triggers,
- /* true if we want a deduction rule */
- bool d_deduction = false);
- PropagateRuleCommand(const std::vector<Expr>& vars,
- const std::vector<Expr>& heads,
- Expr body,
- bool d_deduction = false);
-
- const std::vector<Expr>& getVars() const;
- const std::vector<Expr>& getGuards() const;
- const std::vector<Expr>& 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:
// 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
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
#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"
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<Rational>().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;
}
}
-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();
}
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;
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;
- }
}
}
}
}
}
-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() ){
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)
~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? */
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;
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(); }
/**
/** 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 */
//compute attributes
QAttributes qa;
QuantAttributes::computeQuantAttributes( in, qa );
- if( !qa.isRewriteRule() ){
- for( int op=0; op<COMPUTE_LAST; op++ ){
- if( doOperation( in, op, qa ) ){
- ret = computeOperation( in, op, qa );
- if( ret!=in ){
- rew_op = op;
- status = REWRITE_AGAIN_FULL;
- break;
- }
+ for( int op=0; op<COMPUTE_LAST; op++ ){
+ if( doOperation( in, op, qa ) ){
+ ret = computeOperation( in, op, qa );
+ if( ret!=in ){
+ rew_op = op;
+ status = REWRITE_AGAIN_FULL;
+ break;
}
}
}
}
}
-
-Node QuantifiersRewriter::rewriteRewriteRule( Node r ) {
- Kind rrkind = r[2].getKind();
-
- //guards, pattern, body
-
- // Replace variables by Inst_* variable and tag the terms that contain them
- std::vector<Node> 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<Node> guards;
- std::vector<Node> 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<head.getNumChildren(); i++ ){
- guards.push_back(head[i]);
- pattern.push_back(head[i]);
- }
- break;
- default:
- if( head!=true_node ){
- guards.push_back(head);
- pattern.push_back( head );
- }
- break;
- }
- break;
- default: Unreachable() << "RewriteRules can be of only three kinds"; break;
- }
- // Add the other guards
- TNode g = r[1];
- switch(g.getKind()){
- case kind::AND:
- for( unsigned i = 0; i<g.getNumChildren(); i++ ){
- guards.push_back(g[i]);
- }
- break;
- default:
- if( g != true_node ){
- guards.push_back( g );
- }
- break;
- }
- // Add the other triggers
- if( r[2].getNumChildren() >= 3 ){
- for( unsigned i=0; i<r[2][2][0].getNumChildren(); i++ ) {
- pattern.push_back( r[2][2][0][i] );
- }
- }
-
- Trace("rr-rewrite") << "Rule is " << r << std::endl;
- Trace("rr-rewrite") << "Head is " << head << std::endl;
- Trace("rr-rewrite") << "Patterns are ";
- for( unsigned i=0; i<pattern.size(); i++ ){
- Trace("rr-rewrite") << pattern[i] << " ";
- }
- Trace("rr-rewrite") << std::endl;
-
- NodeBuilder<> 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<Node>(patternB);
- forallB << static_cast<Node>(patternListB);
- Node rn = (Node) forallB;
-
- return rn;
-}
-
bool QuantifiersRewriter::isPrenexNormalForm( Node n ) {
if( n.getKind()==FORALL ){
return n[1].getKind()!=FORALL && isPrenexNormalForm( n[1] );
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
{
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 ) );
private:
static Node preSkolemizeQuantifiers(Node n, bool polarity, std::vector< TypeNode >& fvTypes, std::vector<TNode>& fvs);
public:
- static Node rewriteRewriteRule( Node r );
static bool isPrenexNormalForm( Node n );
/** preprocess
*
+++ /dev/null
-/********************* */
-/*! \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; i<indicies.size(); i++ ){
- d_priority_order.push_back( d_rr_quant[indicies[i]] );
- }
- d_needsSort = false;
- }
-
- //apply rewrite rules
- int addedLemmas = 0;
- //per priority level
- int index = 0;
- bool success = true;
- while( !d_quantEngine->inConflict() && 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<Node, QuantInfo>::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<int> 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<Node> 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<Node> qcfn_c;
-
- std::vector<Node> bvl;
- bvl.insert(bvl.end(), f[0].begin(), f[0].end());
-
- NodeManager* nm = NodeManager::currentNM();
- std::vector<Node> cc;
- // add patterns
- for (unsigned i = 1, nchild = f[2].getNumChildren(); i < nchild; i++)
- {
- std::vector<Node> 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<Node> 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;
- }
-}
+++ /dev/null
-/********************* */
-/*! \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 <map>
-#include <vector>
-
-#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<RrPriorityAttributeId, uint64_t> 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
}
};/* 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<TypeConstant>(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<TypeConstant>(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<bool>(true) ){
- throw TypeCheckingExceptionPrivate(n, "A rewrite rule must have one head or one trigger at least");
- }
- }
- return TypeNode(nodeManager->mkTypeConst<TypeConstant>(RRHB_TYPE));
- }
-};/* struct QuantifierReductionRuleRule */
-
-
}/* CVC4::theory::quantifiers namespace */
}/* CVC4::theory namespace */
}/* CVC4 namespace */
#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"
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),
std::unique_ptr<quantifiers::BoundedIntegers> d_bint;
/** Conflict find mechanism for quantifiers */
std::unique_ptr<quantifiers::QuantConflictFind> d_qcf;
- /** rewrite rules utility */
- std::unique_ptr<quantifiers::RewriteEngine> d_rr_engine;
/** subgoal generator */
std::unique_ptr<quantifiers::ConjectureGenerator> d_sg_gen;
/** ceg instantiation */
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());
// 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));
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)
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())
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())
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
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
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
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
# 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
+++ /dev/null
-; 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)
+++ /dev/null
-; 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)) )
+++ /dev/null
-; 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)
+++ /dev/null
-; 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)
+++ /dev/null
-; 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)
+++ /dev/null
-; 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)
+++ /dev/null
-; 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)
+++ /dev/null
-; 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)
+++ /dev/null
-; 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)
+++ /dev/null
-; 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
+++ /dev/null
-; 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)
+++ /dev/null
-; 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)
+++ /dev/null
-; 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)
+++ /dev/null
-; 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)
+++ /dev/null
-; 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)) ) ))
+++ /dev/null
-; 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)
+++ /dev/null
-; 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)
+++ /dev/null
-; 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)
+++ /dev/null
-; 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)
+++ /dev/null
-; 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)
+++ /dev/null
-; 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)
+++ /dev/null
-; 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)
+++ /dev/null
-; 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)
+++ /dev/null
-; 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)
+++ /dev/null
-; 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)
+++ /dev/null
-; 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)
+++ /dev/null
-; 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)
+++ /dev/null
-; 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)
+++ /dev/null
-; 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)
+++ /dev/null
-; 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
+++ /dev/null
-; 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)
+++ /dev/null
-; 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)
+++ /dev/null
-; 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)
+++ /dev/null
-; 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)
+++ /dev/null
-; 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)
-
projects / cvc5.git / commitdiff