+++ /dev/null
-
-/** DRAFT 1
- * Normal form for predicates:
- * TRUE
- * FALSE
- * var_i |><| b
- * \sum_i product_i |><| b
- * where
- * 1) b is of type CONST_RATIONAL
- * 2) |><| is of type <=, >, =, < or >=
- * 3) product_i is in product normal form,
- * 4) product_i is not 0,
- * 5) product_i's are in strictly ascending productOrder,
- * 6) product_i has at least 2 members,
- * 7) product_1 has a positive coefficient, and
- * 8) var_i has metakind variable.
- *
- * Normal form for terms:
- * c
- * c + \sum_i product_i
- * where
- * 1) c is of type CONST_RATIONAL,
- * 2) product_i is in product normal form,
- * 3) product_i is not a constant,
- * 4) and product_i's are in strictly ascending productOrder.
- *
- * Normal form for products:
- * d
- * var_i
- * e * \prod var_i
- * where
- * 1) d,e is of type CONST_RATIONAL,
- * 2) e != 0,
- * 3) e != 1 or there are at least 2 variables,
- * 2) var_i is of metakind VARIABLE,
- * 3) and var_i are in increasing (not strict) nodeOrder.
- *
- * productOrder is well defined over normal form products as follows:
- * cmp(d,d') = rational order.
- * cmp(d,var_i)= -1
- * cmp(var_i,var_j) is the node order
- * cmp(var_i,d * \prod var_i) = -1
- * cmp(p = d * \prod var_i, p' = d' * \prod var_i')=
- * if(len(p) == len(p'))
- * then tupleCompare(var_i, var_i')
- * else len(p) - len(p')
- */
-
-
-
-/** DRAFT 2
- * Normal form for predicates:
- * TRUE
- * FALSE
- * var |><| b
- * (\sum_{i=1 to N} p_i) |><| b
- * where
- * 1) b is of type CONST_RATIONAL
- * 2) |><| is of kind <, <=, =, >= or >
- * 3) p_i is in PNF,
- * 5) p_i's are in strictly ascending <p,
- * 6) N >= 2,
- * 7) the kind of (\sum_{i=1 to N} p_i) is an N arity PLUS,
- * 8) p_1 has coefficient 1, and
- * 9) var has metakind variable.
- *
- * PNF:
- * v
- * d * v
- * (\prod_{i=1 to M} v_i)
- * d * (\prod_{i=1 to M} v_i)
- * where
- * 1) d is of type CONST_RATIONAL,
- * 2) d != 0,
- * 3) d != 1,
- * 4) M>=2,
- * 5) v, v_i are of metakind VARIABLE,
- * 6) v_i are in increasing (not strict) nodeOrder, and
- * 7) the kind of (\prod_{i=1 to M} v_i) is an M arity MULT.
- *
- * <p is defined over PNF as follows (skipping some symmetry):
- * cmp( v, v') is the node order over v and v'
- * cmp( v,d'*v') is the node order over v and v'
- * cmp(d*v,d'*v') is the node order over v and v'
- * cmp( v, (\prod v'_i)) = -1
- * cmp(d*v, (\prod v_i)) = -1
- * cmp( v, d*(\prod v'_i)) = -1
- * cmp(d*v, d*(\prod v_i)) = -1
- * cmp((\prod_{i=1 to M} v_i),(\prod_{i=1 to M'} v'_i))=
- * if(M == M')
- * then tupleCompare(v_i, v'_i)
- * else M - M'
- * cmp((\prod_{i=1 to M} v_i), d*(\prod_{i=1 to M'} v'_i))=
- * if(M == M')
- * then tupleCompare(v_i, v'_i)
- * else M - M'
- * cmp(d * (\prod_{i=1 to M} v_i), d' * (\prod_{i=1 to M'} v'_i))=
- * if(M == M')
- * then tupleCompare(v_i, v'_i)
- * else M - M'
- *
- * Rewrite Normal Form for Terms:
- * b
- * p
- * c + p
- * (\sum_{i=1 to N} p_i)
- * c + (\sum_{i=1 to N} p_i)
- * where
- * 1) b,c is of type CONST_RATIONAL,
- * 2) c != 0,
- * 3) p, p_i is in PNF,
- * 4) N >= 2
- * 5) the kind of (\sum_{i=1 to N} p_i) is an N arity PLUS,
- * 6) and p_i's are in strictly <p.
- *
- */
-
-
-bool isVarMultList(TNode v){
- for(v = 1 to l.getLength()){
- if(!isVar(v[i])){
- return false;
- }
- }
-
- for(v = 2 to l.getLength()){
- if(!(v[i-1] <= v[i])){
- return false;
- }
- }
- return true;
-}
-
-bool isPNF(TNode p){
- if(p.getKind() == MULT){
- if(p[0].getKind() == CONST_RATIONAL){
- if(p[0].getConst<CONST_RATIONAL>() != 0 &&
- p[0].getConst<CONST_RATIONAL> != 1){
- if(p[1].getKind() != MULT){
- if(p[1].getMetaKind() == VARIABLE){
- return true; // d * v
- }else{
- return false;
- }
- }else{
- if(isVarMultList(p[1])){
- return true; // d * (\prod_{i=1 to M} v_i)
- }else{
- return false;
- }
- }
- }else{
- return false;
- }
- }else{
- if(isVarMultList(p)){
- return true; //(\prod_{i=1 to M} v_i)
- }else{
- return false;
- }
- }
- }else{
- if(p.getMetaKind() == VARIABLE){
- return true; // v
- }else{
- return false;
- }
- }
-}
-
-
-bool <p(TNode p0, TNode p1){
- PNFType t0 = same as the comments in isPNF(p0);
- PNFType t1 = same as the comments in isPNF(p1);
-
- bool t0IsVar = (t0 == "v") ||(t0 == "d*v");
- bool t1IsVar = (t1 == "v") ||(t1 == "d*v");
-
- if(t0IsVar && t1IsVar){
- TNode v0 = (t0 == "d*v") ? p0[1] : p0;
- TNode v1 = (t1 == "d*v") ? p1[1] : p1;
- return v0 < v1;
- }else if(!t0IsVar && t1IsVar){
- return false;
- }else if(t0IsVar && !t1IsVar){
- return true;
- }else{
- TNode prod0 = (t0 == "d * (\prod_{i=1 to M} v_i)") ? p0[1] : p0;
- TNode prod1 = (t1 == "d * (\prod_{i=1 to M} v_i)") ? p1[1] : p1;
-
- int M0 = prod0.getNumChildren();
- int M1 = prod1.getNumChildren();
-
- if(M0 == M1){
- for(i in 1 to M0){
- if(prod0[i] < prod[i]){
- return true;
- }
- }
- return false;
- }else{
- return M0 < M1;
- }
- }
-}
-
-bool isPNFSum(TNode p){
-
- for(i = 1 to p.getNumChildren()){
- if(!isPNF(p[i])){
- return false;
- }
- }
- for(i = 2 to p.getNumChildren()){
- if(!(p[i-1] <p p[i])){
- return false;
- }
- }
- return true;
-}
-
-string isNormalFormTerm(TNode t){
- Kind k = t.getKind();
- if(k != PLUS){
- if(k == CONST_RATIONAL){
- return true; // b
- }else if(isPNF(p)){
- return true; // p
- }else{
- return false;
- }
- }else{
- if(t[0].getKind() == CONST_RATIONAL){
- if(t[0].getConst<CONST_RATIONAL>() != 0){
- if(t[1].getKind() == PLUS){
- if(isPNFSum(t[1])){
- return true; // c + (\sum_{i=1 to N} p_i)
- }else{
- return false;
- }
- }else{
- if(isPNF(t[1])){
- return true; // c + p
- }else{
- return false;
- }
- }
- }else{
- return false;
- }
- }else{
- if(isPNFSum(t)){
- return true; // (\sum_{i=1 to N} p_i)
- }else{
- return false;
- }
- }
- }
-}
-
-/***********************************************/
-/***********************************************/
-/******************* DRAFT 3 *******************/
-/***********************************************/
-/***********************************************/
-
-/** DRAFT 3
- * Normal form for predicates:
- * TRUE
- * FALSE
- * v |><| b
- * p |><| b
- * (+ p_1 .. p_N) |><| b
- * where
- * 1) b is of type CONST_RATIONAL
- * 2) |><| is of kind <, <=, =, >= or >
- * 3) p, p_i is in PNF,
- * 5) p_i's are in strictly ascending <p,
- * 6) N >= 2,
- * 7) the kind of (+ p_1 .. p_N) is an N arity PLUS,
- * 8) p.d, p_1.d are 1, and
- * 9) v has metakind variable.
- *
- * PNF(t):
- * (* d v_1 v_2 ... v_M)
- * where
- * 1) d is of type CONST_RATIONAL,
- * 2) d != 0,
- * 4) M>=1,
- * 5) v_i are of metakind VARIABLE,
- * 6) v_i are in increasing (not strict) nodeOrder, and
- * 7) the kind of t is an M+1 arity MULT.
- *
- * <p is defined over PNF as follows (skipping some symmetry):
- * cmp( (* d v_1 v_2 ... v_M), (* d' v'_1 v'_2 ... v'_M'):
- * if(M == M'):
- * then tupleCompare(v_i, v'_i)
- * else M -M'
- *
- * Rewrite Normal Form for Terms:
- * b
- * v
- * (+ c p_1 p_2 ... p_N) | not(N=1 and c=0 and p_1.d=1)
- * where
- * 1) b,c is of type CONST_RATIONAL,
- * 2) c != 0,
- * 3) p_i is in PNF,
- * 4) N >= 1
- * 5) the kind of (+ c p_1 p_2 ... p_N) is an N+1 arity PLUS,
- * 6) and p_i's are in strictly <p.
- *
- */
-
-
-/* Assuming that the terms have been normalized, how much work is the case splitting.
- * The following should provide a good insight into how difficult it is to use
- * these normal forms when writing code.
- */
-
-enum PredicateNFKind{TRUE, FALSE, v |><| b, p |><| b, (+ p_1 .. p_N) |><| b};
-
-PredicateNFKind kindOfNormalFormPredicate(TNode n){
- if(n.getKind() == CONST_BOOLEAN){
- if(n.getConst<bool>()){
- return TRUE;
- }else{
- return FALSE;
- }
- }else{
- TNode left = n[0];
- if(left.getMetaKind() == metakind::VARIABLE){
- return v |><| b;
- }else if(left.getKind() == MULT){
- return p |><| b;
- }else{
- return (+ p_1 .. p_N) |><| b;
- }
- }
-}
-
-enum TermNFKind{c, v, (+ c p_1 p_2 ... p_N)};
-
-TermNFKind kindOfTermNFKind(TNode n){
- if(n.getMetaKind() == metakind::CONSTANT){
- return c;
- }else if(n.getMetaKind() == metakind::VARIABLE){
- return v;
- }else{
- return (+ c p_1 p_2 ... p_N)
- }
-}
-
-
-/* Verify that the term meets all of the criteria for a normal form.
- * This should provide good insight into how difficult it is to write/debug
- * the rewriters themselves, and other parts of the code that are
- * "highly knowledgable" about the normal form (such as helper functions).
- */
-
-
-bool rangeIsSorted(bool strict, TNode::iterator start, TNode::iterator stop, NodeComparitor cmp){
- if(start == stop) return true;
- TNode prev = *start;
- ++start;
- while(start != stop){
- TNode curr = *start;
- int tmp = cmp(prev, curr);
- if(strict && tmp >= 0
- !strict && tmp > 0
- ){
- return false;
- }
- prev = curr;
- ++start;
- }
- return true;
-}
-
-bool rangeAll(TNode::iterator start, TNode::iterator stop, NodePredicate rho){
- for(;start != stop; ++start){
- if(! rho(*start)) return false;
- }
- return true;
-}
-bool isPNF(TNode p){
- return
- p.getKind() == MULT &&
- p[0].getKind() == CONST_RATIONAL&&
- p[0].getConst<CONST_RATIONAL>() != 0 &&
- rangeIsSorted(false, p.begin()+1, p.end(), nodeOrder) &&
- rangeAll(p.begin()+1, p.end(), \t -> t.getMetaKind() == metakind::VARIABLE);
-}
-
-
-bool cmpPNF(TNode p0, TNode p1){
- int M0 = p0.getNumChildren();
- int M1 = p1.getNumChildren();
-
- if(M0 == M1){
- for(int i=1; i< M0; ++i){
- int cmp = nodeOrder(p0[i],p1[i]);
- if(cmp != 0){
- return cmp;
- }
- }
- return 0;
- }else{
- return M0 - M1;
- }
-}
-
-bool isNormalFormTerm(TNode t){
- if(t.getKind() == CONST_RATIONAL){
- return true;
- }else if(t.getMetaKind() == VARIABLE){
- return true;
- }else if(t.getKind() == PLUS){ //may be (+ c p_1 p_2 ... p_N)
- int N = t.getNumChildren()-1;
- TNode c = t[0];
- return c.getKind() == CONST_RATIONAL &&
- c.getConst<Rational>() !- 0 &&
- N >= 1 && //This check is redundent because of an invariant in NodeBuilder<>
- rangeAll(p.begin()+1, p.end(), isPNF) &&
- rangeIsSorted(true, p.begin()+1, p.end(), cmpPNF);
- }else{
- return false;
- }
-}
-
-bool isNormalFormAtom(TNode n){
- if(n.getKind() == CONST_BOOLEAN){
- return true;
- }else if(n.getKind() \in {<, <=, ==, >=, >}){
- TNode left = n[0];
- TNode right = n[1];
- if(right.getKind() == CONST_RATIONAL){
- if(left.getMetaKind() == VARIABLE){
- return true;
- }else if(left.getKind() == MULT){
- return isPNF(left) && left[0] == 1;
- }else if(left.getKind() == PLUS){
- return left.getNumChildren() >= 2 &&
- rangeAll(left.begin(), left.end(), isPNF) &&
- left[0][0] == 1 &&
- rangeIsSorted(true, left.begin(), left.end(), cmpPNF);
- }else{
- return false;
- }
- }else{
- return false;
- }
- }else{
- return false;
- }
-}
-
-/***********************************************/
-/***********************************************/
-/******************* DRAFT 4 *******************/
-/***********************************************/
-/***********************************************/
-
-/** DRAFT 4
- * variable := n
- * guards
- * n getMetaKind() == metakind::VARIABLE
-
- * constant := n
- * guards
- n.getKind() == kind::CONST_RATIONAL
-
- * monomial := variable | (* [variable])
- * guards
- * len [variable] >= 2
- * isSorted nodeOrder (getMList monomial)
-
-
- * coeff_mono := monomial | (* coeff monomial)
- * guards
- * coeff is renaming for constant
- coeff \not\in {0,1}
-
- * sum := coeff_mono | (+ [coeff_mono])
- * guards
- * len [coeff_mono] >= 2
- * isStronglySorted cmono_cmp [coeff_mono]
-
- * cons_sum := sum | (+ constant_1 sum) | constant_0
- * guards
- * constant_1, constant_0 are accepted by constant
- * constant_1 != 1
-
- * comparison := leads_with_one |><| constant
- * guards
- * |><| is GEQ, EQ, LEQ
- * isStronglySorted cmono_cmp (monomial::[coeff_monomial])
- * leads with_one is a subexpression of sum s.t. it is also accepted by
- * leads_with_one := monomial | (+ monomial [coeff_monomial])
-
- * Normal Form for terms := cons_sum
- * Normal Form for atoms := TRUE | FALSE | comparison | (not comparison)
- *
- * Important Notes:
- *
- * The languages for each are stratified. i.e. it is either the case that
- * they or all of their children belong to a language that is strictly
- * smaller according to the following partial order.
- * constant -> monomial -> coeff_mono -> sum -> cons_sum
- * variable comparison
- * This partial order is not unique, but it is simple.
- *
- * This gives rise to the notion of the tightest language that accepts a node,
- * which is simply the least according to the stratification order above.
- *
- * Each subexpression of a normal form is also a normal form.
- *
- * The tightest language that accepts a node does not always indicate the
- * tighest language of the children:
- * (+ v1 (* v1 v2) (* 2 (* v1 v2 v2)))
-
- * TAGGING:
- * A node in normal form is tagged with the tightest binding above that
- * accepts/generates it.
- * All subexpressions are also in normal form and are also tagged.
- * The tags for terms are as follows:
- * enum { CONSTANT, VARIABLE, MONOMIAL, COEFF_MONOMIAL, SUM, CONS_SUM};
- */
-
- Auxillary
- let rec tuple_cmp elem_cmp pairs_list =
- match pair_list with
- [] -> 0
- |(x,y)::ps -> let cmp_res = elem_cmp x y in
- if cmp_res <> 0
- then cmp_res
- else tuple_cmp elem_cmp ps
-
- let lex_cmp elem_cmp l0 l1 =
- if len l0 == len l1
- then tuple_cmp elem_cmp (zip l0 l1)
- else (len l0) - (len l1)
-
- let rec adjacent l =
- mathc l with
- a::b::xs -> (a,b)::(adjacent b::xs)
- | _ -> []
-
- let isWeaklySorted cmp l =
- forall (fun (x,y) -> cmp x y <= 0) (adjacent l)
-
- let isStronglySorted cmp l =
- forall (fun (x,y) -> cmp x y < 0) (adjacent l)
-
- let getMList monomial =
- match monomial with
- variable -> [variable]
- |(* [variable]) -> [variable]
-
- let drop_coeff coeff_mono =
- match coeff_mono in
- monomial -> monomial
- |(* coeff monomial) -> monomial
-
-let mono_cmp m0 m1 = lex_cmp nodeOrder (getMList m0) (getMList m1)
-let cmono_cmp cm0 cm1 = mono_cmp (drop_coeff cm0) (drop_coeff cm1)
-
+++ /dev/null
-/********************* */
-/*! \file ordered_bounds_list.h
- ** \verbatim
- ** Original author: taking
- ** Major contributors: none
- ** Minor contributors (to current version): mdeters
- ** This file is part of the CVC4 prototype.
- ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys)
- ** Courant Institute of Mathematical Sciences
- ** New York University
- ** See the file COPYING in the top-level source directory for licensing
- ** information.\endverbatim
- **
- ** \brief [[ Add one-line brief description here ]]
- **
- ** [[ Add lengthier description here ]]
- ** \todo document this file
- **/
-
-
-
-#include "cvc4_private.h"
-
-
-#ifndef __CVC4__THEORY__ARITH__ORDERED_BOUNDS_LIST_H
-#define __CVC4__THEORY__ARITH__ORDERED_BOUNDS_LIST_H
-
-#include "expr/node.h"
-#include "util/rational.h"
-#include "expr/kind.h"
-
-#include <vector>
-#include <algorithm>
-
-namespace CVC4 {
-namespace theory {
-namespace arith {
-
-struct RightHandRationalLT
-{
- bool operator()(TNode s1, TNode s2) const
- {
- Assert(s1.getNumChildren() >= 2);
- Assert(s2.getNumChildren() >= 2);
-
- Assert(s1[1].getKind() == kind::CONST_RATIONAL);
- Assert(s2[1].getKind() == kind::CONST_RATIONAL);
-
- TNode rh1 = s1[1];
- TNode rh2 = s2[1];
- const Rational& c1 = rh1.getConst<Rational>();
- const Rational& c2 = rh2.getConst<Rational>();
- return c1.cmp(c2) < 0;
- }
-};
-
-struct RightHandRationalGT
-{
- bool operator()(TNode s1, TNode s2) const
- {
- Assert(s1.getNumChildren() >= 2);
- Assert(s2.getNumChildren() >= 2);
-
- Assert(s1[1].getKind() == kind::CONST_RATIONAL);
- Assert(s2[1].getKind() == kind::CONST_RATIONAL);
-
- TNode rh1 = s1[1];
- TNode rh2 = s2[1];
- const Rational& c1 = rh1.getConst<Rational>();
- const Rational& c2 = rh2.getConst<Rational>();
- return c1.cmp(c2) > 0;
- }
-};
-
-/**
- * An OrderedBoundsList is a lazily sorted vector of Arithmetic constraints.
- * The intended use is for a list of rewriting arithmetic atoms.
- * An example of such a list would be [(<= x 5);(= y 78); (>= x 9)].
- *
- * Nodes are required to have a CONST_RATIONAL child as their second node.
- * Nodes are sorted in increasing order according to RightHandRationalLT.
- *
- * The lists are lazily sorted in the sense that the list is not sorted until
- * an operation to access the element is attempted.
- *
- * An append() may make the list no longer sorted.
- * After an append() operation all iterators for the list become invalid.
- */
-class OrderedBoundsList {
-private:
- bool d_isSorted;
- std::vector<Node> d_list;
-
-public:
- typedef std::vector<Node>::const_iterator iterator;
- typedef std::vector<Node>::const_reverse_iterator reverse_iterator;
-
- /**
- * Constucts a new and empty OrderBoundsList.
- * The empty list is initially sorted.
- */
- OrderedBoundsList() : d_isSorted(true){}
-
- /**
- * Appends a node onto the back of the list.
- * The list may no longer be sorted.
- */
- void append(TNode n){
- Assert(n.getNumChildren() >= 2);
- Assert(n[1].getKind() == kind::CONST_RATIONAL);
- d_isSorted = false;
- d_list.push_back(n);
- }
-
- /** returns the size of the list */
- unsigned int size(){
- return d_list.size();
- }
-
- /** returns the i'th element in the sort list. This may sort the list.*/
- TNode at(unsigned int idx){
- sortIfNeeded();
- return d_list.at(idx);
- }
-
- /** returns true if the list is known to be sorted. */
- bool isSorted() const{
- return d_isSorted;
- }
-
- /** sorts the list. */
- void sort(){
- d_isSorted = true;
- std::sort(d_list.begin(), d_list.end(), RightHandRationalLT());
- }
-
- /**
- * returns an iterator to the list that iterates in ascending order.
- * This may sort the list.
- */
- iterator begin(){
- sortIfNeeded();
- return d_list.begin();
- }
- /**
- * returns an iterator to the end of the list when interating in ascending order.
- */
- iterator end() const{
- return d_list.end();
- }
-
- /**
- * returns an iterator to the list that iterates in descending order.
- * This may sort the list.
- */
- reverse_iterator rbegin(){
- sortIfNeeded();
- return d_list.rend();
- }
- /**
- * returns an iterator to the end of the list when interating in descending order.
- */
- reverse_iterator rend() const{
- return d_list.rend();
- }
-
- /**
- * returns an iterator to the least strict upper bound of value.
- * if the list is [(<= x 2);(>= x 80);(< y 70)]
- * then *upper_bound((< z 70)) == (>= x 80)
- *
- * This may sort the list.
- * see stl::upper_bound for more information.
- */
- iterator upper_bound(TNode value){
- sortIfNeeded();
- return std::upper_bound(begin(), end(), value, RightHandRationalLT());
- }
- /**
- * returns an iterator to the greatest lower bound of value.
- * This is bound is not strict.
- * if the list is [(<= x 2);(>= x 80);(< y 70)]
- * then *lower_bound((< z 70)) == (< y 70)
- *
- * This may sort the list.
- * see stl::upper_bound for more information.
- */
- iterator lower_bound(TNode value){
- sortIfNeeded();
- return std::lower_bound(begin(), end(), value, RightHandRationalLT());
- }
- /**
- * see OrderedBoundsList::upper_bound for more information.
- * The difference is that the iterator goes in descending order.
- */
- reverse_iterator reverse_upper_bound(TNode value){
- sortIfNeeded();
- return std::upper_bound(rbegin(), rend(), value, RightHandRationalGT());
- }
- /**
- * see OrderedBoundsList::lower_bound for more information.
- * The difference is that the iterator goes in descending order.
- */
- reverse_iterator reverse_lower_bound(TNode value){
- sortIfNeeded();
- return std::lower_bound(rbegin(), rend(), value, RightHandRationalGT());
- }
-
- /**
- * This is an O(n) method for searching the array to check if it contains n.
- */
- bool contains(TNode n) const {
- for(std::vector<Node>::const_iterator i = d_list.begin(); i != d_list.end(); ++i){
- if(*i == n) return true;
- }
- return false;
- }
-private:
- /** Sorts the list if it is not already sorted. */
- void sortIfNeeded(){
- if(!d_isSorted){
- sort();
- }
- }
-};
-
-}/* CVC4::theory::arith namespace */
-}/* CVC4::theory namespace */
-}/* CVC4 namespace */
-
-#endif /* __CVC4__THEORY__ARITH__ORDERED_BOUNDS_LIST_H */
projects / cvc5.git / commitdiff