counting-smt's People
Contributors
Stargazers
Watchers
Forkers
dddejancounting-smt's Issues
Unexpected answer
The problem below asks: Find x, y in [0, 10] such that y is the number of u's in [0,10] that are equal to both x and y. The answer I get is card!1 = 5, y = 5, x = 6. For y != x, I would expect the #u is 0. Am I wrong?
(set-logic QF_LIA)
(declare-fun x () Int)
(declare-fun y () Int)
(assert (and (>= x 0) (>= 10 x)))
(assert (and (>= y 0) (>= 10 y)))
(assert (= y (# u Int
(and
(>= u 0) (>= 10 u)
(= u x)
(= u y)
)
)))
(check-sat)
(get-model)Unexpected char: <
Running the solver on the problem below I get a parse error.
(set-logic QF_LIA)
(declare-fun x () Int)
(declare-fun y () Int)
(assert (and (<= 0 x) (<= x 10))
(assert (= y (# u Int (= y x)))
(check-sat)
(get-model)The error is
dejan@pup:~/workspace/counting-smt$ ./solver.native --verbose < ./examples/test04.smt2
-> (set-logic QF_LIA)
-> (declare-fun x () Int)
-> (declare-fun y () Int)
Fatal error: exception Lisp_lexer.SyntaxError("Unexpected char: <")If possible it would be good to output some more info on the error.
Fatal error: exception Not_found
(set-logic QF_LIA)
(declare-fun x () Int)
(declare-fun y () Int)
(declare-fun c () Int)
(assert (= c (# u Int
(and
(>= u 0)
(>= 10 u)
(= (+ u u) (+ x y))
)
)))
(check-sat)
(get-model)gives error
dejan@pup:~/workspace/counting-smt$ ./solver.native --verbose < ./examples/test04.smt2
-> (set-logic QF_LIA)
-> (declare-fun x () Int)
-> (declare-fun y () Int)
-> (declare-fun c () Int)
-> (declare-fun card!1 () Int)
-> (declare-fun card!2 () Int)
-> (declare-fun card!3 () Int)
Fatal error: exception Not_foundFatal error: exception Smtlib.Not_allowed("(not (= u x3))")
(set-logic QF_LIA)
(declare-fun x0 () Int)
(declare-fun x1 () Int)
(declare-fun x2 () Int)
(declare-fun x3 () Int)
(declare-fun s () Int)
(assert (and (>= x0 0) (>= 3 x0)))
(assert (and (>= x1 0) (>= 3 x1)))
(assert (and (>= x2 0) (>= 3 x2)))
(assert (and (>= x3 0) (>= 3 x3)))
(assert (> x0 x1))
(assert (> x1 x2))
(assert (> x2 x3))
(assert (= s (# u Int
(and
(>= u 0) (>= 3 u)
(not (= u x0))
(not (= u x1))
(not (= u x2))
(not (= u x3))
)
)))
(check-sat)
(get-model)ounit?
How do I install ounit on Ubuntu?
dejan@pup:~/workspace/counting-smt$ make tests
ocamlbuild solver.native -use-ocamlfind
Finished, 29 targets (29 cached) in 00:00:00.
ocamlbuild tests.native -use-ocamlfind
+ ocamlfind ocamldep -package ounit -package unix -modules tests.ml > tests.ml.depends
ocamlfind: Package `ounit' not found
Command exited with code 2.
Compilation unsuccessful after building 1 target (0 cached) in 00:00:00.
make: *** [tests] Error 10
Fatal error: exception Theory_model.LA_SMT.Unknown_answer
(set-logic QF_LIA)
(assert (> (# u Int
(and
(<= 0 u) (<= u 10)
(or (< u 0) (> u 10))
))
0
))
(check-sat)Wrong result (sat instead of unsat)
There is no u's that satisfy the constraints, therefore #{u} can not be > 0.
(set-logic QF_LIA)
(assert (> (# u Int
(and
(<= 0 u) (<= u 10)
(or (< u 0) (> u 10))
))
0
))
(check-sat)Seems like wrong answer (sat vs unsat)
pick x,y,z in [L, U]
s1 = #u different from x,y,z
s2 = #u equal to one of x,y,z
can L-U+1 be different from s1+s2?
(set-logic QF_LIA)
(declare-fun x () Int)
(declare-fun y () Int)
(declare-fun z () Int)
(declare-fun L () Int)
(declare-fun U () Int)
(declare-fun s1 () Int)
(declare-fun s2 () Int)
(assert (<= L x))
(assert (< x y))
(assert (< y z))
(assert (<= z U))
(assert (= s1 (# u Int
(and
(<= L u) (<= u U)
(not (= u x))
(not (= u y))
(not (= u z))
)))
)
(assert (= s2 (# u Int
(and
(<= L u) (<= u U)
(or (= u x) (= u y) (= u z))
)))
)
(assert (not (= (+ s1 s2) (+ (- U L) 1))))
(check-sat)
(get-model)Fatal error: exception Smtlib.Not_allowed("1")
(set-logic QF_LIA)
(declare-fun s1 () Int)
(declare-fun s2 () Int)
(assert (= s1 (# u Int (and (>= u 1) (>= 2 u)))))
(assert (= s2 (# u Int (and (>= u 1) (>= 2 u) (>= s1 (+ u 1))))))
(check-sat)
(get-model)Don't want to over do it with issues so I'll stop here. The language doesn't support constants, anything other that >=, and there is no negation.
Wrong result
From first assertion s1 = 2
From second assertion s2 = 1
From third assertion s3 = 0
Output I get is s3 = 2, s2 = 2, s1 = 2
(set-logic QF_LIA)
(declare-fun s1 () Int)
(declare-fun s2 () Int)
(declare-fun s3 () Int)
(assert (= s1 (# u Int (and (>= u 1) (>= 2 u)))))
(assert (= s2 (# u Int (and (>= u 1) (>= 2 u) (< u s1)))))
(assert (= s3 (# u Int (and (>= u 1) (>= 2 u) (< u s2)))))
(check-sat)
(get-model)Recommend Projects
-
React
A declarative, efficient, and flexible JavaScript library for building user interfaces.
-
Vue.js
🖖 Vue.js is a progressive, incrementally-adoptable JavaScript framework for building UI on the web.
-
Typescript
TypeScript is a superset of JavaScript that compiles to clean JavaScript output.
-
TensorFlow
An Open Source Machine Learning Framework for Everyone
-
Django
The Web framework for perfectionists with deadlines.
-
Laravel
A PHP framework for web artisans
-
D3
Bring data to life with SVG, Canvas and HTML. 📊📈🎉
-
Recommend Topics
-
javascript
JavaScript (JS) is a lightweight interpreted programming language with first-class functions.
-
web
Some thing interesting about web. New door for the world.
-
server
A server is a program made to process requests and deliver data to clients.
-
Machine learning
Machine learning is a way of modeling and interpreting data that allows a piece of software to respond intelligently.
-
Visualization
Some thing interesting about visualization, use data art
-
Game
Some thing interesting about game, make everyone happy.
Recommend Org
-
Facebook
We are working to build community through open source technology. NB: members must have two-factor auth.
-
Microsoft
Open source projects and samples from Microsoft.
-
Google
Google ❤️ Open Source for everyone.
-
Alibaba
Alibaba Open Source for everyone
-
D3
Data-Driven Documents codes.
-
Tencent
China tencent open source team.