stanford-centaur / pono Goto Github PK
View Code? Open in Web Editor NEWPono: A flexible and extensible SMT-based model checker
License: Other
pono's People
Contributors
Stargazers
Watchers
Forkers
ahmed-irfan yangy96 lonsing kuree zhanghongce zeta1999 leonardt yoni206 jankcorn log-when taylor-bsg mfkiwl fanhy2114 umarcor skmuduli92 fengwz17 fangwenji liyong31 enmag liuyic00 qianwennn wu-haoze dong-yf seddonshen cccccc96 osankur gipsyh galoisinc cyanokobalamynepono's Issues
Build failed when bash > 5.2
Maybe should update smt-switch version
https://github.com/cvc5/cvc5/blob/86fe72f6d25023387dbc76be9a6c97d4d27e41d3/src/expr/mkmetakind#L19
MBIC3 issue
Hi Makai, this is actually not related to anything I'm working on, maybe not an issue at all, but just to let you know currently MBIC3 seems to be abnormal: producing invariants that are checked to be not inductive.
You can try with the anderson.2.prop1-func-interl.btor2 in the sample.
This is what I got on my end, by running: pono -e mbic3 -v 3 --check-invar anderson.2.prop1-func-interl.btor2
Propagation phase at frame 5
INVARCHECK: init |= inv...OK
INVARCHECK: inv & trans |= inv'...FAIL
INVARCHECK: inv |= prop...OK
Invariant Check FAILED
unknown
b0
Look into infrequent errors in interpolation
Mentioned here: #53
It's possible this is in MathSAT in which case there's not much we can do. But we should be sure that's the case.
cmake failed by not found gmp
CMake Error at CMakeLists.txt:69 (find_package):
By not providing "FindGMP.cmake" in CMAKE_MODULE_PATH this project has
asked CMake to find a package configuration file provided by "GMP", but
CMake did not find one.
Could not find a package configuration file provided by "GMP" with any of
the following names:
GMPConfig.cmake
gmp-config.cmake
Add the installation prefix of "GMP" to CMAKE_PREFIX_PATH or set "GMP_DIR"
to a directory containing one of the above files. If "GMP" provides a
separate development package or SDK, be sure it has been installed.
Actually, I have install libgmp-dev by apt
How to use `pono` correctly with `clk2fflogic`?
I'm attempting to verify a synchronous hardware design, written in Verilog, and expressed in BTOR2 using Yosys. I've followed the guidance in the 'Generating BTOR2 from Verilog' section of the README.
The issue that I'm having is that my design is producing $aldff cells in Yosys. I used the clk2fflogic pass to eliminate these cells and produced syntactically valid BTOR2. However, I'm not getting the results I expect from executing the BTOR using pono.
I'm wondering if someone could clarify the meaning of the "IMPORTANT NOTE" in the README above the clk2fflogic pass:
# (optional) use an "explicit" clock
# e.g. every state is a half cycle of the
# fastest clock
# use this option if you see errors that
# refer to "adff" or asynchronous components
# IMPORTANT NOTE: the clocks are not
# automatically toggled if you use this option
# clk2fflogic;
Does this mean that even if I point pono at the appropriate symbol using the -c flag, the bounded model checking will not correctly toggle the input on each iteration?
Thanks in advance for the help, I really appreciate it!
Make better interface for TS abstraction
Rethink interface for modifying transition system. The current features are a bit heavy handed and dangerous:
tests/python/test_encoders.py AttributeError
It doesn't look like tests/python/test_encoders.py is being run on travis since it's the build is not configured with coreir. However, even if it is being run, it will give a false positive because of #97 (since the travis script runs the test from the project root directory).
When I run the test with the correct path, I get:
______________________________________________________________ test_coreir[create_cvc4_solver] _______________________________________________________________
create_solver = <built-in function create_cvc4_solver>
@pytest.mark.skipif(not COREIR_AVAILABLE, reason="Requires coreir python bindings")
@pytest.mark.parametrize("create_solver", ss.solvers.values())
def test_coreir(create_solver):
file_dir = Path(os.path.dirname(__file__))
coreir_inputs_directory = file_dir / Path("../encoders/inputs/coreir")
for f in coreir_inputs_directory.glob("*.json"):
print("Encoding:", f)
context = coreir.Context()
top_mod = context.load_from_file(str(f))
solver = create_solver(False)
rts = c.RelationalTransitionSystem(solver)
ce = c.CoreIREncoder(top_mod, rts)
t = solver.make_term(True)
> assert ce.trans != t, "Expecting a non-empty transition relation"
E AttributeError: 'pono.CoreIREncoder' object has no attribute 'trans'
tests/python/test_encoders.py:29: AttributeErrorIs there a different API I should be using instead of .trans?
Using old version of smt-switch
A recent bug fix was made in smt-switch: stanford-centaur/smt-switch#321
The version of smt-switch installed by contrib/setup-smt-switch.sh does not use this most recent version.
Suggestion to the Yosys Script
Hi,
I was thinking maybe it is helpful to mention the sim command
in the example yosys script, because sometimes, people may need to
use that to drive the reset pin to get the reset state for formal analysis.
I usually use it in the following way:
sim -clock %clockpin% -reset %resetpin% -n 1 -w %top_module%
There are also other useful options (like nreset, zinit, rstlen) from the Yosys's help message
Thanks
Hongce
Unexpected sort for `neq` operation on arrays
I was testing the following BTOR2 model, which is doing an equality check on two uninitialized arrays:
1 sort bitvec 1
2 sort bitvec 2
3 sort bitvec 8
4 sort array 2 3
5 state 4 mem1
6 state 4 mem2
7 neq 1 5 6
8 bad 7
And for this model pono returns:
Unexpected sort
unknown
b0
Instead of the expected witness with an arbitrary element in the array differing.
Curiously enough, if I only change neq to eq in the model, that works normally:
sat
b0
#0
0 [11] 11111111 mem1@0
0 00000000 mem1@0
1 [11] 11111111 mem2@0
1 00000000 mem2@0
@0
.
Copy TransitionSystem to Property
Edit the transition system in place if
- we need to introduce witnesses (currently done in the encoder)
- for COI
- for property-based abstractions
Revisit input formalism
There are two world-views for how inputs should behave in a transition system:
- they should be state variables with no update constraints
- they should be affiliated only with the transition and thus not be involved in any formula referring to a set of states (only sets of pairs of states -- e.g. the transition relation)
Option 1 makes more sense in hardware and less sense for relational systems. However, adhering to closely to 2 can also cause problems (see #261). We should discuss how to best unify these ideas for different inputs to Pono.
Failure for a small btor2 case
Here is a btor2 file within 42 lines. We have verified the syntactic correctness of this case with btro2tools/catbtor.
1 sort bitvec 1
2 sort bitvec 5
3 consth 2 10
4 consth 2 11
5 mul 2 3 4
6 consth 2 01
7 const 2 01001
8 sll 2 6 7
9 smulo 1 5 8
10 sort bitvec 3
11 const 10 110
12 sort bitvec 2
13 one 12
14 state 1 bv0_1
15 concat 10 13 14
16 ror 10 11 15
17 init 1 14 9
18 sort bitvec 8
19 constd 18 -111
20 const 18 01000110
21 xor 18 19 20
22 slice 1 21 3 3
23 next 1 14 22
24 state 10 bv1_3
25 init 10 24 16
26 xnor 10 24 24
27 not 10 26
28 sra 10 27 24
29 next 10 24 28
30 sort bitvec 6
31 sort array 1 30
32 state 31 arr0_1_6
33 input 30
34 write 31 32 14 33
35 sgte 1 24 24
36 mul 30 33 33
37 write 31 34 35 36
38 sub 30 33 33
39 mul 30 38 33
40 write 31 37 35 39
41 next 31 32 40
42 bad 14
Checking this file with command "./pono -e ic3ia -k 1000000" produces the following error message:
_[boolector] boolector_slice: 'upper' must not be < 'lower'
error
b0_
If I modify the operator in line 16 from "ror" to "add", Pono produces the result normally:
_sat
b0_
May I ask is it a bug in Pono or the usage of "ror" operator is wrong in this case?
Version of pono commit: 8b2a946
Encoder directly from Yosys RTLIL
It could be very nice to have encoder directly from Yosys to a transition system instead of going through BTOR2. This is not currently a priority, but it would give us more control over the encoding.
Use constant references for iteration
When iterating over a data structure, we should use const auto & if the variable can be const.
Possible enhancement: Check for weaker interpolants
Attached is a simple example that interpolant-based model checking diverges on. It turns out that the generated interpolants are too strong and keep getting expanded with constant values. However, the first interpolant actually contained the "right" interpolant as one of its conjuncts. If we had detected that a subformula was itself an interpolant, this would not happen.
Swap Relational and Functional Transition system relationship
There are often cases where want to take a functional transition system but not a relational transition system. This is difficult with the current inheritance relationship.
Allow out-of-tree dependencies
Currently, the build scripts assume that dependenices like smt-switch and btor2tools are in the deps folder. We should allow building/installing these separately and specifying their paths.
Build broken with latest smt-switch
Looks like stanford-centaur/smt-switch@4858959 broke cosa2 build. This worked as a quick-and-dirty work-around for me:
diff --git a/contrib/setup-smt-switch.sh b/contrib/setup-smt-switch.sh
index e22cde1..694d4ba 100755
--- a/contrib/setup-smt-switch.sh
+++ b/contrib/setup-smt-switch.sh
@@ -51,6 +51,7 @@ if [ ! -d "$DEPS/smt-switch" ]; then
cd $DEPS
git clone https://github.com/makaimann/smt-switch
cd smt-switch
+ git checkout -f 48589590~1
./contrib/setup-btor.sh
if [[ "$WITH_MSAT" != default ]]; then
cc @makaimann
MSAT related code in create_reducer_for is not guarded by macro
Hi I'm having compilation issues when not using MSAT. Therefore, I'm wondering: maybe this part of code needs to be guarded by macro WITH_MSAT? Thanks!
UNKNOWN instead of SAT for BMC benchmark
I have a benchmark that returns a witness with btormc -kmax 25 but returns unknown with cosa2 -k 25 -e bmc.
First, I would have expected -e bmc to only return sat or unsat, never unknown. Am I missing something?
Second, is this a bug? Would there be value in making this benchmark available? (Would require some work on my side to remove some secret stuff, and I could only provide it to individual persons, not publish it here.)
Handle multi-property monitors better
If a property contains next states or inputs, then a property monitor state variable is introduced. In the case where multiple properties are checked on the same transition system, this could pollute the system with too many extra state variables. We should figure out a better way to handle this.
Related to #104
Unwanted skbuild printouts
When i import skbuild with python3 on my system I get the following printouts:
>>> import skbuild
Generating grammar tables from /usr/lib/python3.8/lib2to3/Grammar.txt
Generating grammar tables from /usr/lib/python3.8/lib2to3/PatternGrammar.txt
This causes issues in python/CMakeLists.txt since line 90 is not expecting this extra printout.
Locally, I have fixed this by replacing the import skbuild at line 81 of the script with import sys; temp = sys.stdout; sys.stdout = open(os.devnull,\"w\"); import skbuild; sys.stdout = temp to silence the output.
simple_alu.py - RuntimeError: BoolectorSolver::make_sort
How can I try to fix this?
Fresh build of pono with everything except CoreIR.
--with-msat:
Traceback (most recent call last):
File "/home/xxx/xxx/xxx/pono/examples/python-api/simple_alu.py", line 158, in <module>
k_induction_attempt()
File "/home/xxx/xxx/xxx/pono/examples/python-api/simple_alu.py", line 61, in k_induction_attempt
prop = build_simple_alu_fts(s)
File "/home/xxx/job/xxx/pono/examples/python-api/simple_alu.py", line 16, in build_simple_alu_fts
fts = pono.FunctionalTransitionSystem(s)
File "pono_imp.pxi", line 57, in pono.__AbstractTransitionSystem.__cinit__
RuntimeError: BoolectorSolver::make_sort
Process finished with exit code 1
Without msat:
============== Running k-induction ==============
INIT
(bvand (bvnot cfg) (ite (= spec_res imp_res) #b1 #b0))
TRANS
(and (= spec_res.next (bvadd a b)) (= cfg cfg.next) (= imp_res.next (bvadd a (ite (= #b1 cfg) (bvadd (bvnot b) #b00000001) b))))
PROP
(= spec_res imp_res)
None
KInduction returned unknown
Traceback (most recent call last):
File "/home/xxx/pono/examples/python-api/simple_alu.py", line 159, in <module>
interpolant_attempt()
File "/home/xxx/pono/examples/python-api/simple_alu.py", line 82, in interpolant_attempt
s = ss.create_msat_solver(False)
AttributeError: module 'smt_switch' has no attribute 'create_msat_solver'
Process finished with exit code 1
Pono outputs longer than expected witness
I have the following chisel code
class DivisionByZeroIsEq(to: Int) extends Module {
val a = IO(Input(UInt(2.W)))
val b = IO(Input(UInt(2.W)))
val d = a / b
assume(b === 0.U)
assert(d === to.U)
}Which compiles to the following btor2 output:
1 sort bitvec 1
2 input 1 reset
3 sort bitvec 2
4 input 3 a ; @[src/test/scala/chiseltest/formal/UndefinedValuesTests.scala 61:13]
5 input 3 b ; @[src/test/scala/chiseltest/formal/UndefinedValuesTests.scala 62:13]
6 input 3 d_invalid ; @[src/test/scala/chiseltest/formal/UndefinedValuesTests.scala 63:13]
; _resetCount.init
7 zero 1
8 state 1 _resetCount
9 init 1 8 7
10 zero 3
11 eq 1 5 10 ; @[src/test/scala/chiseltest/formal/UndefinedValuesTests.scala 63:13]
12 udiv 3 4 5
13 ite 3 11 6 12 ; @[src/test/scala/chiseltest/formal/UndefinedValuesTests.scala 63:13]
14 zero 1
15 uext 3 14 1
16 eq 1 5 15 ; @[src/test/scala/chiseltest/formal/UndefinedValuesTests.scala 64:12]
17 not 1 2 ; @[src/test/scala/chiseltest/formal/UndefinedValuesTests.scala 64:9]
18 not 1 16 ; @[src/test/scala/chiseltest/formal/UndefinedValuesTests.scala 64:9]
19 zero 1
20 uext 3 19 1
21 eq 1 13 20 ; @[src/test/scala/chiseltest/formal/UndefinedValuesTests.scala 65:12]
22 not 1 21 ; @[src/test/scala/chiseltest/formal/UndefinedValuesTests.scala 65:9]
23 one 1
24 ugte 1 8 23
25 not 1 24
26 implies 1 17 16
27 constraint 26 ; assume @[src/test/scala/chiseltest/formal/UndefinedValuesTests.scala 64:9]
28 implies 1 17 21
29 not 1 28
30 bad 29 ; assert @[src/test/scala/chiseltest/formal/UndefinedValuesTests.scala 65:9]
31 implies 1 25 2
32 constraint 31 ; _resetActive
; _resetCount.next
33 uext 3 8 1
34 one 1
35 uext 3 34 1
36 add 3 33 35
37 slice 1 36 0 0
38 ite 1 25 37 8
39 next 1 8 38
The output of pono gives a witness of length 2:
$ pono -e bmc -k 2 --vcd ignore.vcd DivisionByZeroIsEq.btor
sat
b0
#0
0 0 _resetCount@0
@0
0 1 reset@0
1 00 a@0
2 00 b@0
3 00 d_invalid@0
@1
0 0 reset@1
1 11 a@1
2 00 b@1
3 10 d_invalid@1
@2
0 1 reset@2
1 00 a@2
2 00 b@2
3 00 d_invalid@2
.
Whereas btormc takes only a single step:
$ btormc --kmax 1 DivisionByZeroIsEq.btor
b0
@0
0 1 reset@0
1 00 a@0
2 00 b@0
3 00 d_invalid@0
@1
0 0 reset@1
1 00 a@1
2 00 b@1
3 10 d_invalid@1
.
Pono really should be failing the bounded model check in a single step.
Heisenbug with smt-switch boolector backend
In certain (supposedly rare cases) running BMC with the boolector backend will return an incorrect result. Reproducible on this branch: https://github.com/upscale-project/cosa2/tree/debugging. Small changes, such as adding/removing a print statement that just prints an arbitrary string, will change the result.
The bug might be in https://github.com/makaimann/smt-switch or in boolector.
Destruct pointers in Cython bindings
Need to implement __dealloc__ to delete pointers used in the Cython bindings.
Consider changing logger implementation
A few reasons to change the logger implementation:
- it seems like the logger evaluates all the arguments regardless of the verbosity (e.g. even if it doesn't print it). This means the
to_stringfor large terms could be called all the time even at low verbosity. - I believe it is the only part of the codebase that uses C++17
Could consider looking into a stream based one -- maybe that would help. A macro could also work, but we do want to be able to change the verbosity dynamically so it would have to take an argument.
Rename default branch to main
We should rename the master branch to main. See here for the rationale: https://about.gitlab.com/blog/2021/03/10/new-git-default-branch-name/.
Error during the build of the last commit, Cython related
I'm trying to build an updated version
6d72613 in Docker. And receive some errors from Cython files. Have you seen this before?
[ 55%] Generating CXX source python/pono.cxx
Error compiling Cython file:
------------------------------------------------------------
...
void add_constraint(const c_Term & constraint) except +
void name_term(const string name, const c_Term & t) except +
c_Term make_inputvar(const string name, const c_Sort & sort) except +
c_Term make_statevar(const string name, const c_Sort & sort) except +
c_Term curr(const c_Term & term) except +
c_Term next(const c_Term & ter m) except +
^
------------------------------------------------------------
/home/xxx/pono/python/pono_imp.pxd:27:40: Expected ')', found 'm'
Error compiling Cython file:
------------------------------------------------------------
...
from libcpp.string cimport string
from libcpp.unordered_set cimport unordered_set
from libcpp.unordered_map cimport unordered_map
from libcpp.vector cimport vector
from pono_imp cimport TransitionSystem as c_TransitionSystem
^
------------------------------------------------------------
/home/xxx/pono/python/pono_imp.pxi:8:0: 'pono_imp/TransitionSystem.pxd' not found
Error compiling Cython file:
------------------------------------------------------------
...
from libcpp.unordered_set cimport unordered_set
from libcpp.unordered_map cimport unordered_map
from libcpp.vector cimport vector
from pono_imp cimport TransitionSystem as c_TransitionSystem
from pono_imp cimport RelationalTransitionSystem as c_RelationalTransitionSystem
^
------------------------------------------------------------
/home/xxx/pono/python/pono_imp.pxi:9:0: 'pono_imp/RelationalTransitionSystem.pxd' not found
Error compiling Cython file:
------------------------------------------------------------
...
from libcpp.unordered_map cimport unordered_map
from libcpp.vector cimport vector
from pono_imp cimport TransitionSystem as c_TransitionSystem
from pono_imp cimport RelationalTransitionSystem as c_RelationalTransitionSystem
from pono_imp cimport FunctionalTransitionSystem as c_FunctionalTransitionSystem
^
------------------------------------------------------------
/home/xxx/pono/python/pono_imp.pxi:10:0: 'pono_imp/FunctionalTransitionSystem.pxd' not found
Error compiling Cython file:
------------------------------------------------------------
...
from libcpp.vector cimport vector
from pono_imp cimport TransitionSystem as c_TransitionSystem
from pono_imp cimport RelationalTransitionSystem as c_RelationalTransitionSystem
from pono_imp cimport FunctionalTransitionSystem as c_FunctionalTransitionSystem
from pono_imp cimport Property as c_Property
^
------------------------------------------------------------
/home/xxx/pono/python/pono_imp.pxi:11:0: 'pono_imp/Property.pxd' not found
Error compiling Cython file:
------------------------------------------------------------
...
from pono_imp cimport TransitionSystem as c_TransitionSystem
from pono_imp cimport RelationalTransitionSystem as c_RelationalTransitionSystem
from pono_imp cimport FunctionalTransitionSystem as c_FunctionalTransitionSystem
from pono_imp cimport Property as c_Property
from pono_imp cimport Unroller as c_Unroller
^
------------------------------------------------------------
/home/xxx/pono/python/pono_imp.pxi:12:0: 'pono_imp/Unroller.pxd' not found
Error compiling Cython file:
------------------------------------------------------------
...
from pono_imp cimport TransitionSystem as c_TransitionSystem
from pono_imp cimport RelationalTransitionSystem as c_RelationalTransitionSystem
from pono_imp cimport FunctionalTransitionSystem as c_FunctionalTransitionSystem
from pono_imp cimport Property as c_Property
from pono_imp cimport Unroller as c_Unroller
from pono_imp cimport ProverResult as c_ProverResult
^
------------------------------------------------------------
/home/xxx/pono/python/pono_imp.pxi:13:0: 'pono_imp/ProverResult.pxd' not found
Error compiling Cython file:
------------------------------------------------------------
...
from pono_imp cimport RelationalTransitionSystem as c_RelationalTransitionSystem
from pono_imp cimport FunctionalTransitionSystem as c_FunctionalTransitionSystem
from pono_imp cimport Property as c_Property
from pono_imp cimport Unroller as c_Unroller
from pono_imp cimport ProverResult as c_ProverResult
from pono_imp cimport UNKNOWN as c_UNKNOWN
^
------------------------------------------------------------
/home/xxx/pono/python/pono_imp.pxi:14:0: 'pono_imp/UNKNOWN.pxd' not found
Error compiling Cython file:
------------------------------------------------------------
...
from pono_imp cimport FunctionalTransitionSystem as c_FunctionalTransitionSystem
from pono_imp cimport Property as c_Property
from pono_imp cimport Unroller as c_Unroller
from pono_imp cimport ProverResult as c_ProverResult
from pono_imp cimport UNKNOWN as c_UNKNOWN
from pono_imp cimport FALSE as c_FALSE
^
------------------------------------------------------------
/home/xxx/pono/python/pono_imp.pxi:15:0: 'pono_imp/FALSE.pxd' not found
Error compiling Cython file:
------------------------------------------------------------
...
from pono_imp cimport Property as c_Property
from pono_imp cimport Unroller as c_Unroller
from pono_imp cimport ProverResult as c_ProverResult
from pono_imp cimport UNKNOWN as c_UNKNOWN
from pono_imp cimport FALSE as c_FALSE
from pono_imp cimport TRUE as c_TRUE
^
------------------------------------------------------------
/home/xxx/pono/python/pono_imp.pxi:16:0: 'pono_imp/TRUE.pxd' not found
Error compiling Cython file:
------------------------------------------------------------
...
from pono_imp cimport Unroller as c_Unroller
from pono_imp cimport ProverResult as c_ProverResult
from pono_imp cimport UNKNOWN as c_UNKNOWN
from pono_imp cimport FALSE as c_FALSE
from pono_imp cimport TRUE as c_TRUE
from pono_imp cimport Prover as c_Prover
^
------------------------------------------------------------
/home/xxx/pono/python/pono_imp.pxi:17:0: 'pono_imp/Prover.pxd' not found
Error compiling Cython file:
------------------------------------------------------------
...
from pono_imp cimport ProverResult as c_ProverResult
from pono_imp cimport UNKNOWN as c_UNKNOWN
from pono_imp cimport FALSE as c_FALSE
from pono_imp cimport TRUE as c_TRUE
from pono_imp cimport Prover as c_Prover
from pono_imp cimport Bmc as c_Bmc
^
------------------------------------------------------------
/home/xxx/pono/python/pono_imp.pxi:18:0: 'pono_imp/Bmc.pxd' not found
Error compiling Cython file:
------------------------------------------------------------
...
from pono_imp cimport UNKNOWN as c_UNKNOWN
from pono_imp cimport FALSE as c_FALSE
from pono_imp cimport TRUE as c_TRUE
from pono_imp cimport Prover as c_Prover
from pono_imp cimport Bmc as c_Bmc
from pono_imp cimport KInduction as c_KInduction
^
------------------------------------------------------------
/home/xxx/pono/python/pono_imp.pxi:19:0: 'pono_imp/KInduction.pxd' not found
Error compiling Cython file:
------------------------------------------------------------
...
from pono_imp cimport FALSE as c_FALSE
from pono_imp cimport TRUE as c_TRUE
from pono_imp cimport Prover as c_Prover
from pono_imp cimport Bmc as c_Bmc
from pono_imp cimport KInduction as c_KInduction
from pono_imp cimport BmcSimplePath as c_BmcSimplePath
^
------------------------------------------------------------
/home/xxx/pono/python/pono_imp.pxi:20:0: 'pono_imp/BmcSimplePath.pxd' not found
Error compiling Cython file:
------------------------------------------------------------
...
from pono_imp cimport TRUE as c_TRUE
from pono_imp cimport Prover as c_Prover
from pono_imp cimport Bmc as c_Bmc
from pono_imp cimport KInduction as c_KInduction
from pono_imp cimport BmcSimplePath as c_BmcSimplePath
from pono_imp cimport InterpolantMC as c_InterpolantMC
^
------------------------------------------------------------
/home/xxx/pono/python/pono_imp.pxi:21:0: 'pono_imp/InterpolantMC.pxd' not found
Error compiling Cython file:
------------------------------------------------------------
...
from pono_imp cimport Prover as c_Prover
from pono_imp cimport Bmc as c_Bmc
from pono_imp cimport KInduction as c_KInduction
from pono_imp cimport BmcSimplePath as c_BmcSimplePath
from pono_imp cimport InterpolantMC as c_InterpolantMC
from pono_imp cimport BTOR2Encoder as c_BTOR2Encoder
^
------------------------------------------------------------
/home/xxx/pono/python/pono_imp.pxi:22:0: 'pono_imp/BTOR2Encoder.pxd' not found
Error compiling Cython file:
------------------------------------------------------------
...
from pono_imp cimport InterpolantMC as c_InterpolantMC
from pono_imp cimport BTOR2Encoder as c_BTOR2Encoder
IF WITH_COREIR == "ON":
from pono_imp cimport Module as c_Module
from pono_imp cimport CoreIREncoder as c_CoreIREncoder
from pono_imp cimport set_global_logger_verbosity as c_set_global_logger_verbosity
^
------------------------------------------------------------
/home/xxx/pono/python/pono_imp.pxi:26:0: 'pono_imp/set_global_logger_verbosity.pxd' not found
Error compiling Cython file:
------------------------------------------------------------
...
from pono_imp cimport BTOR2Encoder as c_BTOR2Encoder
IF WITH_COREIR == "ON":
from pono_imp cimport Module as c_Module
from pono_imp cimport CoreIREncoder as c_CoreIREncoder
from pono_imp cimport set_global_logger_verbosity as c_set_global_logger_verbosity
from pono_imp cimport get_free_symbols as c_get_free_symbols
^
------------------------------------------------------------
/home/xxx/pono/python/pono_imp.pxi:27:0: 'pono_imp/get_free_symbols.pxd' not found
Error compiling Cython file:
------------------------------------------------------------
...
ctypedef const unordered_map[c_Term, c_Term]* const_UnorderedTermMapPtr
ctypedef unordered_map[c_Term, c_Term].const_iterator c_UnorderedTermMap_const_iterator
cdef class __AbstractTransitionSystem:
cdef c_TransitionSystem* cts
^
------------------------------------------------------------
/home/xxx/pono/python/pono_imp.pxi:51:9: 'c_TransitionSystem' is not a type identifier
Error compiling Cython file:
------------------------------------------------------------
...
self.cts = new c_FunctionalTransitionSystem(s.css)
self._solver = s
cdef class Property:
cdef c_Property* cp
^
------------------------------------------------------------
/home/xxx/pono/python/pono_imp.pxi:310:9: 'c_Property' is not a type identifier
Error compiling Cython file:
------------------------------------------------------------
...
def transition_system(self):
return self.ts
cdef class Unroller:
cdef c_Unroller* cu
^
------------------------------------------------------------
/home/xxx/pono/python/pono_imp.pxi:328:9: 'c_Unroller' is not a type identifier
Error compiling Cython file:
------------------------------------------------------------
...
term.ct = dref(self.cu).untime(t.ct)
return term
cdef class __AbstractProver:
cdef c_Prover* cp
^
------------------------------------------------------------
/home/xxx/pono/python/pono_imp.pxi:346:9: 'c_Prover' is not a type identifier
Error compiling Cython file:
------------------------------------------------------------
...
self.cp = new c_InterpolantMC(p.cp[0], s.css, interp.css)
self._solver = s
cdef class BTOR2Encoder:
cdef c_BTOR2Encoder * cbe
^
------------------------------------------------------------
/home/xxx/pono/python/pono_imp.pxi:430:9: 'c_BTOR2Encoder' is not a type identifier
Error compiling Cython file:
------------------------------------------------------------
...
cdef SmtSolver _solver
# Note: don't want to allow null TransitionSystems
# means there's no way to instantiate a transition system without the solver
def __cinit__(self, SmtSolver s):
# if not specified, this creates a relational transition system under the hood
self.cts = new c_RelationalTransitionSystem(s.css)
^
------------------------------------------------------------
/home/xxx/pono/python/pono_imp.pxi:57:23: 'c_RelationalTransitionSystem' is not a type identifier
Error compiling Cython file:
------------------------------------------------------------
...
cdef SmtSolver _solver
# Note: don't want to allow null TransitionSystems
# means there's no way to instantiate a transition system without the solver
def __cinit__(self, SmtSolver s):
# if not specified, this creates a relational transition system under the hood
self.cts = new c_RelationalTransitionSystem(s.css)
^
------------------------------------------------------------
/home/xxx/pono/python/pono_imp.pxi:57:23: new operator can only be applied to a C++ class
Error compiling Cython file:
------------------------------------------------------------
...
# if not specified, this creates a relational transition system under the hood
self.cts = new c_RelationalTransitionSystem(s.css)
self._solver = s
def set_init(self, Term init):
dref(self.cts).set_init(init.ct)
^
------------------------------------------------------------
/home/xxx/pono/python/pono_imp.pxi:61:36: Cannot convert 'c_Term' to Python object
Error compiling Cython file:
------------------------------------------------------------
...
def set_init(self, Term init):
dref(self.cts).set_init(init.ct)
def constrain_init(self, Term constraint):
dref(self.cts).constrain_init(constraint.ct)
^
------------------------------------------------------------
/home/xxx/pono/python/pono_imp.pxi:64:48: Cannot convert 'c_Term' to Python object
Error compiling Cython file:
------------------------------------------------------------
...
def constrain_init(self, Term constraint):
dref(self.cts).constrain_init(constraint.ct)
def assign_next(self, Term state, Term val):
dref(self.cts).assign_next(state.ct, val.ct)
^
------------------------------------------------------------
/home/xxx/pono/python/pono_imp.pxi:67:40: Cannot convert 'c_Term' to Python object
Error compiling Cython file:
------------------------------------------------------------
...
def constrain_init(self, Term constraint):
dref(self.cts).constrain_init(constraint.ct)
def assign_next(self, Term state, Term val):
dref(self.cts).assign_next(state.ct, val.ct)
^
------------------------------------------------------------
/home/xxx/pono/python/pono_imp.pxi:67:48: Cannot convert 'c_Term' to Python object
Error compiling Cython file:
------------------------------------------------------------
...
def assign_next(self, Term state, Term val):
dref(self.cts).assign_next(state.ct, val.ct)
def add_invar(self, Term constraint):
dref(self.cts).add_invar(constraint.ct)
^
------------------------------------------------------------
/home/xxx/pono/python/pono_imp.pxi:70:43: Cannot convert 'c_Term' to Python object
Error compiling Cython file:
------------------------------------------------------------
...
def add_invar(self, Term constraint):
dref(self.cts).add_invar(constraint.ct)
def constrain_inputs(self, Term constraint):
dref(self.cts).constrain_inputs(constraint.ct)
^
------------------------------------------------------------
/home/xxx/pono/python/pono_imp.pxi:73:50: Cannot convert 'c_Term' to Python object
Error compiling Cython file:
------------------------------------------------------------
...
def constrain_inputs(self, Term constraint):
dref(self.cts).constrain_inputs(constraint.ct)
def add_constraint(self, Term constraint):
dref(self.cts).add_constraint(constraint.ct)
^
------------------------------------------------------------
/home/xxx/pono/python/pono_imp.pxi:76:48: Cannot convert 'c_Term' to Python object
Error compiling Cython file:
------------------------------------------------------------
...
def add_constraint(self, Term constraint):
dref(self.cts).add_constraint(constraint.ct)
def name_term(self, str name, Term t):
dref(self.cts).name_term(name.encode(), t.ct)
^
------------------------------------------------------------
/home/xxx/pono/python/pono_imp.pxi:79:49: Cannot convert 'c_Term' to Python object
Error compiling Cython file:
------------------------------------------------------------
...
def name_term(self, str name, Term t):
dref(self.cts).name_term(name.encode(), t.ct)
def make_inputvar(self, str name, Sort sort):
cdef Term term = Term(self._solver)
term.ct = dref(self.cts).make_inputvar(name.encode(), sort.cs)
^
------------------------------------------------------------
/home/xxx/pono/python/pono_imp.pxi:83:66: Cannot convert 'c_Sort' to Python object
Error compiling Cython file:
------------------------------------------------------------
...
def name_term(self, str name, Term t):
dref(self.cts).name_term(name.encode(), t.ct)
def make_inputvar(self, str name, Sort sort):
cdef Term term = Term(self._solver)
term.ct = dref(self.cts).make_inputvar(name.encode(), sort.cs)
^
------------------------------------------------------------
/home/xxx/pono/python/pono_imp.pxi:83:46: Cannot convert Python object to 'c_Term'
Error compiling Cython file:
------------------------------------------------------------
...
term.ct = dref(self.cts).make_inputvar(name.encode(), sort.cs)
return term
def make_statevar(self, str name, Sort sort):
cdef Term term = Term(self._solver)
term.ct = dref(self.cts).make_statevar(name.encode(), sort.cs)
^
------------------------------------------------------------
/home/xxx/pono/python/pono_imp.pxi:88:66: Cannot convert 'c_Sort' to Python object
Error compiling Cython file:
------------------------------------------------------------
...
term.ct = dref(self.cts).make_inputvar(name.encode(), sort.cs)
return term
def make_statevar(self, str name, Sort sort):
cdef Term term = Term(self._solver)
term.ct = dref(self.cts).make_statevar(name.encode(), sort.cs)
^
------------------------------------------------------------
/home/xxx/pono/python/pono_imp.pxi:88:46: Cannot convert Python object to 'c_Term'
Error compiling Cython file:
------------------------------------------------------------
...
term.ct = dref(self.cts).make_statevar(name.encode(), sort.cs)
return term
def curr(self, Term t):
cdef Term term = Term(self._solver)
term.ct = dref(self.cts).curr(t.ct)
^
------------------------------------------------------------
/home/xxx/pono/python/pono_imp.pxi:93:39: Cannot convert 'c_Term' to Python object
Error compiling Cython file:
------------------------------------------------------------
...
term.ct = dref(self.cts).make_statevar(name.encode(), sort.cs)
return term
def curr(self, Term t):
cdef Term term = Term(self._solver)
term.ct = dref(self.cts).curr(t.ct)
^
------------------------------------------------------------
/home/xxx/pono/python/pono_imp.pxi:93:37: Cannot convert Python object to 'c_Term'
Error compiling Cython file:
------------------------------------------------------------
...
term.ct = dref(self.cts).curr(t.ct)
return term
def next(self, Term t):
cdef Term term = Term(self._solver)
term.ct = dref(self.cts).next(t.ct)
^
------------------------------------------------------------
/home/xxx/pono/python/pono_imp.pxi:98:39: Cannot convert 'c_Term' to Python object
Error compiling Cython file:
------------------------------------------------------------
...
term.ct = dref(self.cts).curr(t.ct)
return term
def next(self, Term t):
cdef Term term = Term(self._solver)
term.ct = dref(self.cts).next(t.ct)
^
------------------------------------------------------------
/home/xxx/pono/python/pono_imp.pxi:98:37: Cannot convert Python object to 'c_Term'
Error compiling Cython file:
------------------------------------------------------------
...
cdef Term term = Term(self._solver)
term.ct = dref(self.cts).next(t.ct)
return term
def is_curr_var(self, Term sv):
return dref(self.cts).is_curr_var(sv.ct)
^
------------------------------------------------------------
/home/xxx/pono/python/pono_imp.pxi:102:44: Cannot convert 'c_Term' to Python object
Error compiling Cython file:
------------------------------------------------------------
...
def is_curr_var(self, Term sv):
return dref(self.cts).is_curr_var(sv.ct)
def is_next_var(self, Term sv):
return dref(self.cts).is_next_var(sv.ct)
^
------------------------------------------------------------
/home/xxx/pono/python/pono_imp.pxi:105:44: Cannot convert 'c_Term' to Python object
Error compiling Cython file:
------------------------------------------------------------
...
@property
def statevars(self):
states_set = set()
cdef const_UnorderedTermSetPtr c_states_set = &dref(self.cts).statevars()
^
------------------------------------------------------------
/home/xxx/pono/python/pono_imp.pxi:115:54: Taking address of non-lvalue (type Python object)
Error compiling Cython file:
------------------------------------------------------------
...
@property
def inputvars(self):
inputs_set = set()
cdef const_UnorderedTermSetPtr c_inputs_set = &dref(self.cts).inputvars()
^
------------------------------------------------------------
/home/xxx/pono/python/pono_imp.pxi:132:54: Taking address of non-lvalue (type Python object)
Error compiling Cython file:
------------------------------------------------------------
...
@property
def state_updates(self):
updates = {}
cdef const_UnorderedTermMapPtr c_updates_map = &dref(self.cts).state_updates()
^
------------------------------------------------------------
/home/xxx/pono/python/pono_imp.pxi:149:55: Taking address of non-lvalue (type Python object)
Error compiling Cython file:
------------------------------------------------------------
...
@property
def named_terms(self):
names2terms = {}
cdef unordered_map[string, c_Term]* c_named_terms = &dref(self.cts).named_terms()
^
------------------------------------------------------------
/home/xxx/pono/python/pono_imp.pxi:169:60: Taking address of non-lvalue (type Python object)
Error compiling Cython file:
------------------------------------------------------------
...
return names2terms
@property
def constraints(self):
convec = []
cdef c_TermVec c_cons = dref(self.cts).constraints()
^
------------------------------------------------------------
/home/xxx/pono/python/pono_imp.pxi:185:58: Cannot convert Python object to 'c_TermVec'
Error compiling Cython file:
------------------------------------------------------------
...
return convec
@property
def init(self):
cdef Term term = Term(self._solver)
term.ct = dref(self.cts).init()
^
------------------------------------------------------------
/home/xxx/pono/python/pono_imp.pxi:195:37: Cannot convert Python object to 'c_Term'
Error compiling Cython file:
------------------------------------------------------------
...
return term
@property
def trans(self):
cdef Term term = Term(self._solver)
term.ct = dref(self.cts).trans()
^
------------------------------------------------------------
/home/xxx/pono/python/pono_imp.pxi:201:38: Cannot convert Python object to 'c_Term'
Error compiling Cython file:
------------------------------------------------------------
...
cdef Sort s = Sort(self)
cdef c_SortKind sk
cdef c_SortVec csv
if isinstance(arg0, str):
s.cs = dref(self.cts).make_sort(<const string> arg0.encode(), <int?> arg1)
^
------------------------------------------------------------
/home/xxx/pono/python/pono_imp.pxi:213:43: Cannot convert Python object to 'c_Sort'
Error compiling Cython file:
------------------------------------------------------------
...
if isinstance(arg0, str):
s.cs = dref(self.cts).make_sort(<const string> arg0.encode(), <int?> arg1)
elif isinstance(arg0, SortKind):
sk = (<SortKind> arg0).sk
if arg1 is None:
s.cs = dref(self.cts).make_sort(sk)
^
------------------------------------------------------------
/home/xxx/pono/python/pono_imp.pxi:217:48: Cannot convert 'c_SortKind' to Python object
Error compiling Cython file:
------------------------------------------------------------
...
if isinstance(arg0, str):
s.cs = dref(self.cts).make_sort(<const string> arg0.encode(), <int?> arg1)
elif isinstance(arg0, SortKind):
sk = (<SortKind> arg0).sk
if arg1 is None:
s.cs = dref(self.cts).make_sort(sk)
^
------------------------------------------------------------
/home/xxx/pono/python/pono_imp.pxi:217:47: Cannot convert Python object to 'c_Sort'
Error compiling Cython file:
------------------------------------------------------------
...
elif isinstance(arg0, SortKind):
sk = (<SortKind> arg0).sk
if arg1 is None:
s.cs = dref(self.cts).make_sort(sk)
elif isinstance(arg1, int) and arg2 is None:
s.cs = dref(self.cts).make_sort(sk, <int> arg1)
^
------------------------------------------------------------
/home/xxx/pono/python/pono_imp.pxi:219:48: Cannot convert 'c_SortKind' to Python object
Error compiling Cython file:
------------------------------------------------------------
...
elif isinstance(arg0, SortKind):
sk = (<SortKind> arg0).sk
if arg1 is None:
s.cs = dref(self.cts).make_sort(sk)
elif isinstance(arg1, int) and arg2 is None:
s.cs = dref(self.cts).make_sort(sk, <int> arg1)
^
------------------------------------------------------------
/home/xxx/pono/python/pono_imp.pxi:219:47: Cannot convert Python object to 'c_Sort'
Error compiling Cython file:
------------------------------------------------------------
...
if arg1 is None:
s.cs = dref(self.cts).make_sort(sk)
elif isinstance(arg1, int) and arg2 is None:
s.cs = dref(self.cts).make_sort(sk, <int> arg1)
elif isinstance(arg1, Sort) and arg2 is None:
s.cs = dref(self.cts).make_sort(sk, (<Sort> arg1).cs)
^
------------------------------------------------------------
/home/xxx/pono/python/pono_imp.pxi:221:48: Cannot convert 'c_SortKind' to Python object
Error compiling Cython file:
------------------------------------------------------------
...
if arg1 is None:
s.cs = dref(self.cts).make_sort(sk)
elif isinstance(arg1, int) and arg2 is None:
s.cs = dref(self.cts).make_sort(sk, <int> arg1)
elif isinstance(arg1, Sort) and arg2 is None:
s.cs = dref(self.cts).make_sort(sk, (<Sort> arg1).cs)
^
------------------------------------------------------------
/home/xxx/pono/python/pono_imp.pxi:221:65: Cannot convert 'c_Sort' to Python object
Error compiling Cython file:
------------------------------------------------------------
...
if arg1 is None:
s.cs = dref(self.cts).make_sort(sk)
elif isinstance(arg1, int) and arg2 is None:
s.cs = dref(self.cts).make_sort(sk, <int> arg1)
elif isinstance(arg1, Sort) and arg2 is None:
s.cs = dref(self.cts).make_sort(sk, (<Sort> arg1).cs)
^
------------------------------------------------------------
/home/xxx/pono/python/pono_imp.pxi:221:47: Cannot convert Python object to 'c_Sort'
Error compiling Cython file:
------------------------------------------------------------
...
elif isinstance(arg1, Sort) and arg2 is None:
s.cs = dref(self.cts).make_sort(sk, (<Sort> arg1).cs)
elif isinstance(arg1, list) and arg2 is None:
for a in arg1:
csv.push_back((<Sort?> a).cs)
s.cs = dref(self.cts).make_sort(sk, csv)
^
------------------------------------------------------------
/home/xxx/pono/python/pono_imp.pxi:225:48: Cannot convert 'c_SortKind' to Python object
Error compiling Cython file:
------------------------------------------------------------
...
elif isinstance(arg1, Sort) and arg2 is None:
s.cs = dref(self.cts).make_sort(sk, (<Sort> arg1).cs)
elif isinstance(arg1, list) and arg2 is None:
for a in arg1:
csv.push_back((<Sort?> a).cs)
s.cs = dref(self.cts).make_sort(sk, csv)
^
------------------------------------------------------------
/home/xxx/pono/python/pono_imp.pxi:225:52: Cannot convert 'c_SortVec' to Python object
Error compiling Cython file:
------------------------------------------------------------
...
elif isinstance(arg1, Sort) and arg2 is None:
s.cs = dref(self.cts).make_sort(sk, (<Sort> arg1).cs)
elif isinstance(arg1, list) and arg2 is None:
for a in arg1:
csv.push_back((<Sort?> a).cs)
s.cs = dref(self.cts).make_sort(sk, csv)
^
------------------------------------------------------------
/home/xxx/pono/python/pono_imp.pxi:225:47: Cannot convert Python object to 'c_Sort'
Error compiling Cython file:
------------------------------------------------------------
...
elif isinstance(arg1, list) and arg2 is None:
for a in arg1:
csv.push_back((<Sort?> a).cs)
s.cs = dref(self.cts).make_sort(sk, csv)
elif arg3 is None:
s.cs = dref(self.cts).make_sort(sk, (<Sort?> arg1).cs, (<Sort?> arg2).cs)
^
------------------------------------------------------------
/home/xxx/pono/python/pono_imp.pxi:227:48: Cannot convert 'c_SortKind' to Python object
Error compiling Cython file:
------------------------------------------------------------
...
elif isinstance(arg1, list) and arg2 is None:
for a in arg1:
csv.push_back((<Sort?> a).cs)
s.cs = dref(self.cts).make_sort(sk, csv)
elif arg3 is None:
s.cs = dref(self.cts).make_sort(sk, (<Sort?> arg1).cs, (<Sort?> arg2).cs)
^
------------------------------------------------------------
/home/xxx/pono/python/pono_imp.pxi:227:66: Cannot convert 'c_Sort' to Python object
Error compiling Cython file:
------------------------------------------------------------
...
elif isinstance(arg1, list) and arg2 is None:
for a in arg1:
csv.push_back((<Sort?> a).cs)
s.cs = dref(self.cts).make_sort(sk, csv)
elif arg3 is None:
s.cs = dref(self.cts).make_sort(sk, (<Sort?> arg1).cs, (<Sort?> arg2).cs)
^
------------------------------------------------------------
/home/xxx/pono/python/pono_imp.pxi:227:85: Cannot convert 'c_Sort' to Python object
Error compiling Cython file:
------------------------------------------------------------
...
elif isinstance(arg1, list) and arg2 is None:
for a in arg1:
csv.push_back((<Sort?> a).cs)
s.cs = dref(self.cts).make_sort(sk, csv)
elif arg3 is None:
s.cs = dref(self.cts).make_sort(sk, (<Sort?> arg1).cs, (<Sort?> arg2).cs)
^
------------------------------------------------------------
/home/xxx/pono/python/pono_imp.pxi:227:47: Cannot convert Python object to 'c_Sort'
Error compiling Cython file:
------------------------------------------------------------
...
csv.push_back((<Sort?> a).cs)
s.cs = dref(self.cts).make_sort(sk, csv)
elif arg3 is None:
s.cs = dref(self.cts).make_sort(sk, (<Sort?> arg1).cs, (<Sort?> arg2).cs)
elif arg3 is not None:
s.cs = dref(self.cts).make_sort(sk, (<Sort?> arg1).cs,
^
------------------------------------------------------------
/home/xxx/pono/python/pono_imp.pxi:229:48: Cannot convert 'c_SortKind' to Python object
Error compiling Cython file:
------------------------------------------------------------
...
csv.push_back((<Sort?> a).cs)
s.cs = dref(self.cts).make_sort(sk, csv)
elif arg3 is None:
s.cs = dref(self.cts).make_sort(sk, (<Sort?> arg1).cs, (<Sort?> arg2).cs)
elif arg3 is not None:
s.cs = dref(self.cts).make_sort(sk, (<Sort?> arg1).cs,
^
------------------------------------------------------------
/home/xxx/pono/python/pono_imp.pxi:229:66: Cannot convert 'c_Sort' to Python object
Error compiling Cython file:
------------------------------------------------------------
...
s.cs = dref(self.cts).make_sort(sk, csv)
elif arg3 is None:
s.cs = dref(self.cts).make_sort(sk, (<Sort?> arg1).cs, (<Sort?> arg2).cs)
elif arg3 is not None:
s.cs = dref(self.cts).make_sort(sk, (<Sort?> arg1).cs,
(<Sort?> arg2).cs,
^
------------------------------------------------------------
/home/xxx/pono/python/pono_imp.pxi:230:66: Cannot convert 'c_Sort' to Python object
Error compiling Cython file:
------------------------------------------------------------
...
elif arg3 is None:
s.cs = dref(self.cts).make_sort(sk, (<Sort?> arg1).cs, (<Sort?> arg2).cs)
elif arg3 is not None:
s.cs = dref(self.cts).make_sort(sk, (<Sort?> arg1).cs,
(<Sort?> arg2).cs,
(<Sort?> arg3).cs)
^
------------------------------------------------------------
/home/xxx/pono/python/pono_imp.pxi:231:66: Cannot convert 'c_Sort' to Python object
Error compiling Cython file:
------------------------------------------------------------
...
csv.push_back((<Sort?> a).cs)
s.cs = dref(self.cts).make_sort(sk, csv)
elif arg3 is None:
s.cs = dref(self.cts).make_sort(sk, (<Sort?> arg1).cs, (<Sort?> arg2).cs)
elif arg3 is not None:
s.cs = dref(self.cts).make_sort(sk, (<Sort?> arg1).cs,
^
------------------------------------------------------------
/home/xxx/pono/python/pono_imp.pxi:229:47: Cannot convert Python object to 'c_Sort'
Error compiling Cython file:
------------------------------------------------------------
...
if not args:
raise ValueError("Can't call make_term with an Op ({}) and no arguments".format(op_or_val))
for a in args:
ctv.push_back((<Term?> a).ct)
term.ct = dref(self.cts).make_term((<Op> op_or_val).op, ctv)
^
------------------------------------------------------------
/home/xxx/pono/python/pono_imp.pxi:267:63: Cannot convert 'c_Op' to Python object
Error compiling Cython file:
------------------------------------------------------------
...
if not args:
raise ValueError("Can't call make_term with an Op ({}) and no arguments".format(op_or_val))
for a in args:
ctv.push_back((<Term?> a).ct)
term.ct = dref(self.cts).make_term((<Op> op_or_val).op, ctv)
^
------------------------------------------------------------
/home/xxx/pono/python/pono_imp.pxi:267:68: Cannot convert 'c_TermVec' to Python object
Error compiling Cython file:
------------------------------------------------------------
...
if not args:
raise ValueError("Can't call make_term with an Op ({}) and no arguments".format(op_or_val))
for a in args:
ctv.push_back((<Term?> a).ct)
term.ct = dref(self.cts).make_term((<Op> op_or_val).op, ctv)
^
------------------------------------------------------------
/home/xxx/pono/python/pono_imp.pxi:267:46: Cannot convert Python object to 'c_Term'
Error compiling Cython file:
------------------------------------------------------------
...
for a in args:
ctv.push_back((<Term?> a).ct)
term.ct = dref(self.cts).make_term((<Op> op_or_val).op, ctv)
elif isinstance(op_or_val, bool) and len(args) == 0:
term.ct = dref(self.cts).make_term(<bint> op_or_val)
^
------------------------------------------------------------
/home/xxx/pono/python/pono_imp.pxi:269:46: Cannot convert Python object to 'c_Term'
Error compiling Cython file:
------------------------------------------------------------
...
ctv.push_back((<Term?> a).ct)
term.ct = dref(self.cts).make_term((<Op> op_or_val).op, ctv)
elif isinstance(op_or_val, bool) and len(args) == 0:
term.ct = dref(self.cts).make_term(<bint> op_or_val)
elif isinstance(op_or_val, str) and len(args) == 1 and isinstance(args[0], Sort):
term.ct = dref(self.cts).make_term(<const string> op_or_val.encode(), (<Sort> args[0]).cs)
^
------------------------------------------------------------
/home/xxx/pono/python/pono_imp.pxi:271:98: Cannot convert 'c_Sort' to Python object
Error compiling Cython file:
------------------------------------------------------------
...
ctv.push_back((<Term?> a).ct)
term.ct = dref(self.cts).make_term((<Op> op_or_val).op, ctv)
elif isinstance(op_or_val, bool) and len(args) == 0:
term.ct = dref(self.cts).make_term(<bint> op_or_val)
elif isinstance(op_or_val, str) and len(args) == 1 and isinstance(args[0], Sort):
term.ct = dref(self.cts).make_term(<const string> op_or_val.encode(), (<Sort> args[0]).cs)
^
------------------------------------------------------------
/home/xxx/pono/python/pono_imp.pxi:271:46: Cannot convert Python object to 'c_Term'
Error compiling Cython file:
------------------------------------------------------------
...
term.ct = dref(self.cts).make_term(<bint> op_or_val)
elif isinstance(op_or_val, str) and len(args) == 1 and isinstance(args[0], Sort):
term.ct = dref(self.cts).make_term(<const string> op_or_val.encode(), (<Sort> args[0]).cs)
elif isinstance(op_or_val, str) and len(args) == 2 and isinstance(args[0], Sort):
term.ct = dref(self.cts).make_term(<const string> op_or_val.encode(),
(<Sort> args[0]).cs,
^
------------------------------------------------------------
/home/xxx/pono/python/pono_imp.pxi:274:63: Cannot convert 'c_Sort' to Python object
Error compiling Cython file:
------------------------------------------------------------
...
elif isinstance(op_or_val, bool) and len(args) == 0:
term.ct = dref(self.cts).make_term(<bint> op_or_val)
elif isinstance(op_or_val, str) and len(args) == 1 and isinstance(args[0], Sort):
term.ct = dref(self.cts).make_term(<const string> op_or_val.encode(), (<Sort> args[0]).cs)
elif isinstance(op_or_val, str) and len(args) == 2 and isinstance(args[0], Sort):
term.ct = dref(self.cts).make_term(<const string> op_or_val.encode(),
^
------------------------------------------------------------
/home/xxx/pono/python/pono_imp.pxi:273:46: Cannot convert Python object to 'c_Term'
Error compiling Cython file:
------------------------------------------------------------
...
term.ct = dref(self.cts).make_term(<const string> op_or_val.encode(),
(<Sort> args[0]).cs,
<int?> args[1])
elif isinstance(op_or_val, int) and len(args) == 1 and isinstance(args[0], Sort):
# always use the string representation of integers (to handle large ints)
term.ct = dref(self.cts).make_term((<const string?> str(op_or_val).encode()), (<Sort> args[0]).cs)
^
------------------------------------------------------------
/home/xxx/pono/python/pono_imp.pxi:278:106: Cannot convert 'c_Sort' to Python object
Error compiling Cython file:
------------------------------------------------------------
...
term.ct = dref(self.cts).make_term(<const string> op_or_val.encode(),
(<Sort> args[0]).cs,
<int?> args[1])
elif isinstance(op_or_val, int) and len(args) == 1 and isinstance(args[0], Sort):
# always use the string representation of integers (to handle large ints)
term.ct = dref(self.cts).make_term((<const string?> str(op_or_val).encode()), (<Sort> args[0]).cs)
^
------------------------------------------------------------
/home/xxx/pono/python/pono_imp.pxi:278:46: Cannot convert Python object to 'c_Term'
Error compiling Cython file:
------------------------------------------------------------
...
elif isinstance(op_or_val, int) and len(args) == 1 and isinstance(args[0], Sort):
# always use the string representation of integers (to handle large ints)
term.ct = dref(self.cts).make_term((<const string?> str(op_or_val).encode()), (<Sort> args[0]).cs)
elif isinstance(op_or_val, Term) and len(args) == 1 and isinstance(args[0], Sort):
# this is for creating a constant array
term.ct = dref(self.cts).make_term((<Term?> op_or_val).ct, (<Sort?> args[0]).cs)
^
------------------------------------------------------------
/home/xxx/pono/python/pono_imp.pxi:281:66: Cannot convert 'c_Term' to Python object
Error compiling Cython file:
------------------------------------------------------------
...
elif isinstance(op_or_val, int) and len(args) == 1 and isinstance(args[0], Sort):
# always use the string representation of integers (to handle large ints)
term.ct = dref(self.cts).make_term((<const string?> str(op_or_val).encode()), (<Sort> args[0]).cs)
elif isinstance(op_or_val, Term) and len(args) == 1 and isinstance(args[0], Sort):
# this is for creating a constant array
term.ct = dref(self.cts).make_term((<Term?> op_or_val).ct, (<Sort?> args[0]).cs)
^
------------------------------------------------------------
/home/xxx/pono/python/pono_imp.pxi:281:88: Cannot convert 'c_Sort' to Python object
Error compiling Cython file:
------------------------------------------------------------
...
elif isinstance(op_or_val, int) and len(args) == 1 and isinstance(args[0], Sort):
# always use the string representation of integers (to handle large ints)
term.ct = dref(self.cts).make_term((<const string?> str(op_or_val).encode()), (<Sort> args[0]).cs)
elif isinstance(op_or_val, Term) and len(args) == 1 and isinstance(args[0], Sort):
# this is for creating a constant array
term.ct = dref(self.cts).make_term((<Term?> op_or_val).ct, (<Sort?> args[0]).cs)
^
------------------------------------------------------------
/home/xxx/pono/python/pono_imp.pxi:281:46: Cannot convert Python object to 'c_Term'
Error compiling Cython file:
------------------------------------------------------------
...
return term
cdef class RelationalTransitionSystem(__AbstractTransitionSystem):
def __cinit__(self, SmtSolver s):
self.cts = new c_RelationalTransitionSystem(s.css)
^
------------------------------------------------------------
/home/xxx/pono/python/pono_imp.pxi:290:23: 'c_RelationalTransitionSystem' is not a type identifier
Error compiling Cython file:
------------------------------------------------------------
...
return term
cdef class RelationalTransitionSystem(__AbstractTransitionSystem):
def __cinit__(self, SmtSolver s):
self.cts = new c_RelationalTransitionSystem(s.css)
^
------------------------------------------------------------
/home/xxx/pono/python/pono_imp.pxi:290:23: new operator can only be applied to a C++ class
Error compiling Cython file:
------------------------------------------------------------
...
def __cinit__(self, SmtSolver s):
self.cts = new c_RelationalTransitionSystem(s.css)
self._solver = s
def set_behavior(self, Term init, Term trans):
dref(<c_RelationalTransitionSystem * ?> self.cts).set_behavior(init.ct, trans.ct)
^
------------------------------------------------------------
/home/xxx/pono/python/pono_imp.pxi:294:14: 'c_RelationalTransitionSystem' is not a type identifier
Error compiling Cython file:
------------------------------------------------------------
...
def __cinit__(self, SmtSolver s):
self.cts = new c_RelationalTransitionSystem(s.css)
self._solver = s
def set_behavior(self, Term init, Term trans):
dref(<c_RelationalTransitionSystem * ?> self.cts).set_behavior(init.ct, trans.ct)
^
------------------------------------------------------------
/home/xxx/pono/python/pono_imp.pxi:294:75: Cannot convert 'c_Term' to Python object
Error compiling Cython file:
------------------------------------------------------------
...
def __cinit__(self, SmtSolver s):
self.cts = new c_RelationalTransitionSystem(s.css)
self._solver = s
def set_behavior(self, Term init, Term trans):
dref(<c_RelationalTransitionSystem * ?> self.cts).set_behavior(init.ct, trans.ct)
^
------------------------------------------------------------
/home/xxx/pono/python/pono_imp.pxi:294:85: Cannot convert 'c_Term' to Python object
Error compiling Cython file:
------------------------------------------------------------
...
def set_behavior(self, Term init, Term trans):
dref(<c_RelationalTransitionSystem * ?> self.cts).set_behavior(init.ct, trans.ct)
def set_trans(self, Term trans):
dref(<c_RelationalTransitionSystem * ?> self.cts).set_trans(trans.ct)
^
------------------------------------------------------------
/home/xxx/pono/python/pono_imp.pxi:297:14: 'c_RelationalTransitionSystem' is not a type identifier
Error compiling Cython file:
------------------------------------------------------------
...
def set_behavior(self, Term init, Term trans):
dref(<c_RelationalTransitionSystem * ?> self.cts).set_behavior(init.ct, trans.ct)
def set_trans(self, Term trans):
dref(<c_RelationalTransitionSystem * ?> self.cts).set_trans(trans.ct)
^
------------------------------------------------------------
/home/xxx/pono/python/pono_imp.pxi:297:73: Cannot convert 'c_Term' to Python object
Error compiling Cython file:
------------------------------------------------------------
...
def set_trans(self, Term trans):
dref(<c_RelationalTransitionSystem * ?> self.cts).set_trans(trans.ct)
def constrain_trans(self, Term constraint):
dref(<c_RelationalTransitionSystem * ?> self.cts).constrain_trans(constraint.ct)
^
------------------------------------------------------------
/home/xxx/pono/python/pono_imp.pxi:300:14: 'c_RelationalTransitionSystem' is not a type identifier
Error compiling Cython file:
------------------------------------------------------------
...
def set_trans(self, Term trans):
dref(<c_RelationalTransitionSystem * ?> self.cts).set_trans(trans.ct)
def constrain_trans(self, Term constraint):
dref(<c_RelationalTransitionSystem * ?> self.cts).constrain_trans(constraint.ct)
^
------------------------------------------------------------
/home/xxx/pono/python/pono_imp.pxi:300:84: Cannot convert 'c_Term' to Python object
Error compiling Cython file:
------------------------------------------------------------
...
dref(<c_RelationalTransitionSystem * ?> self.cts).constrain_trans(constraint.ct)
cdef class FunctionalTransitionSystem(__AbstractTransitionSystem):
def __cinit__(self, SmtSolver s):
self.cts = new c_FunctionalTransitionSystem(s.css)
^
------------------------------------------------------------
/home/xxx/pono/python/pono_imp.pxi:305:23: 'c_FunctionalTransitionSystem' is not a type identifier
Error compiling Cython file:
------------------------------------------------------------
...
dref(<c_RelationalTransitionSystem * ?> self.cts).constrain_trans(constraint.ct)
cdef class FunctionalTransitionSystem(__AbstractTransitionSystem):
def __cinit__(self, SmtSolver s):
self.cts = new c_FunctionalTransitionSystem(s.css)
^
------------------------------------------------------------
/home/xxx/pono/python/pono_imp.pxi:305:23: new operator can only be applied to a C++ class
Error compiling Cython file:
------------------------------------------------------------
...
cdef class Property:
cdef c_Property* cp
cdef __AbstractTransitionSystem ts
def __cinit__(self, __AbstractTransitionSystem ts, Term p):
self.cp = new c_Property(ts.cts[0], p.ct)
^
------------------------------------------------------------
/home/xxx/pono/python/pono_imp.pxi:313:22: 'c_Property' is not a type identifier
Error compiling Cython file:
------------------------------------------------------------
...
cdef class Property:
cdef c_Property* cp
cdef __AbstractTransitionSystem ts
def __cinit__(self, __AbstractTransitionSystem ts, Term p):
self.cp = new c_Property(ts.cts[0], p.ct)
^
------------------------------------------------------------
/home/xxx/pono/python/pono_imp.pxi:313:22: new operator can only be applied to a C++ class
Error compiling Cython file:
------------------------------------------------------------
...
self.ts = ts
@property
def prop(self):
cdef Term p = Term(self.ts.solver)
p.ct = dref(self.cp).prop()
^
------------------------------------------------------------
/home/xxx/pono/python/pono_imp.pxi:319:33: Cannot convert Python object to 'c_Term'
Error compiling Cython file:
------------------------------------------------------------
...
cdef class Unroller:
cdef c_Unroller* cu
cdef SmtSolver _solver
def __cinit__(self, __AbstractTransitionSystem ts, SmtSolver s):
self.cu = new c_Unroller(ts.cts[0], s.css)
^
------------------------------------------------------------
/home/xxx/pono/python/pono_imp.pxi:331:22: 'c_Unroller' is not a type identifier
Error compiling Cython file:
------------------------------------------------------------
...
cdef class Unroller:
cdef c_Unroller* cu
cdef SmtSolver _solver
def __cinit__(self, __AbstractTransitionSystem ts, SmtSolver s):
self.cu = new c_Unroller(ts.cts[0], s.css)
^
------------------------------------------------------------
/home/xxx/pono/python/pono_imp.pxi:331:22: new operator can only be applied to a C++ class
Error compiling Cython file:
------------------------------------------------------------
...
self.cu = new c_Unroller(ts.cts[0], s.css)
self._solver = s
def at_time(self, Term t, unsigned int k):
cdef Term term = Term(self._solver)
term.ct = dref(self.cu).at_time(t.ct, k)
^
------------------------------------------------------------
/home/xxx/pono/python/pono_imp.pxi:336:41: Cannot convert 'c_Term' to Python object
Error compiling Cython file:
------------------------------------------------------------
...
self.cu = new c_Unroller(ts.cts[0], s.css)
self._solver = s
def at_time(self, Term t, unsigned int k):
cdef Term term = Term(self._solver)
term.ct = dref(self.cu).at_time(t.ct, k)
^
------------------------------------------------------------
/home/xxx/pono/python/pono_imp.pxi:336:39: Cannot convert Python object to 'c_Term'
Error compiling Cython file:
------------------------------------------------------------
...
term.ct = dref(self.cu).at_time(t.ct, k)
return term
def untime(self, Term t):
cdef Term term = Term(self._solver)
term.ct = dref(self.cu).untime(t.ct)
^
------------------------------------------------------------
/home/xxx/pono/python/pono_imp.pxi:341:40: Cannot convert 'c_Term' to Python object
Error compiling Cython file:
------------------------------------------------------------
...
term.ct = dref(self.cu).at_time(t.ct, k)
return term
def untime(self, Term t):
cdef Term term = Term(self._solver)
term.ct = dref(self.cu).untime(t.ct)
^
------------------------------------------------------------
/home/xxx/pono/python/pono_imp.pxi:341:38: Cannot convert Python object to 'c_Term'
Error compiling Cython file:
------------------------------------------------------------
...
def check_until(self, int k):
'''
Checks until bound k, returns True, False or None (if unknown)
'''
cdef int r = <int> dref(self.cp).check_until(k)
if r == (<int> c_UNKNOWN):
^
------------------------------------------------------------
/home/xxx/pono/python/pono_imp.pxi:358:23: 'c_UNKNOWN' is not a constant, variable or function identifier
Error compiling Cython file:
------------------------------------------------------------
...
Checks until bound k, returns True, False or None (if unknown)
'''
cdef int r = <int> dref(self.cp).check_until(k)
if r == (<int> c_UNKNOWN):
return None
elif r == (<int> c_FALSE):
^
------------------------------------------------------------
/home/xxx/pono/python/pono_imp.pxi:360:25: 'c_FALSE' is not a constant, variable or function identifier
Error compiling Cython file:
------------------------------------------------------------
...
cdef int r = <int> dref(self.cp).check_until(k)
if r == (<int> c_UNKNOWN):
return None
elif r == (<int> c_FALSE):
return False
elif r == (<int> c_TRUE):
^
------------------------------------------------------------
/home/xxx/pono/python/pono_imp.pxi:362:25: 'c_TRUE' is not a constant, variable or function identifier
Error compiling Cython file:
------------------------------------------------------------
...
elif r == (<int> c_TRUE):
return True
def witness(self):
cdef vector[c_UnorderedTermMap] cw
success = dref(self.cp).witness(cw)
^
------------------------------------------------------------
/home/xxx/pono/python/pono_imp.pxi:367:40: Cannot convert 'vector[c_UnorderedTermMap]' to Python object
Error compiling Cython file:
------------------------------------------------------------
...
'''
Tries to prove property unboundedly, returns True, False or None (if unknown)
'''
cdef int r = <int> dref(self.cp).prove()
if r == (<int> c_UNKNOWN):
^
------------------------------------------------------------
/home/xxx/pono/python/pono_imp.pxi:393:23: 'c_UNKNOWN' is not a constant, variable or function identifier
Error compiling Cython file:
------------------------------------------------------------
...
'''
cdef int r = <int> dref(self.cp).prove()
if r == (<int> c_UNKNOWN):
return None
elif r == (<int> c_FALSE):
^
------------------------------------------------------------
/home/xxx/pono/python/pono_imp.pxi:395:25: 'c_FALSE' is not a constant, variable or function identifier
Error compiling Cython file:
------------------------------------------------------------
...
if r == (<int> c_UNKNOWN):
return None
elif r == (<int> c_FALSE):
return False
elif r == (<int> c_TRUE):
^
------------------------------------------------------------
/home/xxx/pono/python/pono_imp.pxi:397:25: 'c_TRUE' is not a constant, variable or function identifier
Error compiling Cython file:
------------------------------------------------------------
...
return self._property
cdef class Bmc(__AbstractProver):
def __cinit__(self, Property p, SmtSolver s):
self.cp = new c_Bmc(p.cp[0], s.css)
^
------------------------------------------------------------
/home/xxx/pono/python/pono_imp.pxi:407:22: 'c_Bmc' is not a type identifier
Error compiling Cython file:
------------------------------------------------------------
...
return self._property
cdef class Bmc(__AbstractProver):
def __cinit__(self, Property p, SmtSolver s):
self.cp = new c_Bmc(p.cp[0], s.css)
^
------------------------------------------------------------
/home/xxx/pono/python/pono_imp.pxi:407:22: new operator can only be applied to a C++ class
Error compiling Cython file:
------------------------------------------------------------
...
self._solver = s
cdef class KInduction(__AbstractProver):
def __cinit__(self, Property p, SmtSolver s):
self.cp = new c_KInduction(p.cp[0], s.css)
^
------------------------------------------------------------
/home/xxx/pono/python/pono_imp.pxi:413:22: 'c_KInduction' is not a type identifier
Error compiling Cython file:
------------------------------------------------------------
...
self._solver = s
cdef class KInduction(__AbstractProver):
def __cinit__(self, Property p, SmtSolver s):
self.cp = new c_KInduction(p.cp[0], s.css)
^
------------------------------------------------------------
/home/xxx/pono/python/pono_imp.pxi:413:22: new operator can only be applied to a C++ class
Error compiling Cython file:
------------------------------------------------------------
...
self._solver = s
cdef class BmcSimplePath(__AbstractProver):
def __cinit__(self, Property p, SmtSolver s):
self.cp = new c_BmcSimplePath(p.cp[0], s.css)
^
------------------------------------------------------------
/home/xxx/pono/python/pono_imp.pxi:419:22: 'c_BmcSimplePath' is not a type identifier
Error compiling Cython file:
------------------------------------------------------------
...
self._solver = s
cdef class BmcSimplePath(__AbstractProver):
def __cinit__(self, Property p, SmtSolver s):
self.cp = new c_BmcSimplePath(p.cp[0], s.css)
^
------------------------------------------------------------
/home/xxx/pono/python/pono_imp.pxi:419:22: new operator can only be applied to a C++ class
Error compiling Cython file:
------------------------------------------------------------
...
self._solver = s
cdef class InterpolantMC(__AbstractProver):
def __cinit__(self, Property p, SmtSolver s, SmtSolver interp):
self.cp = new c_InterpolantMC(p.cp[0], s.css, interp.css)
^
------------------------------------------------------------
/home/xxx/pono/python/pono_imp.pxi:425:22: 'c_InterpolantMC' is not a type identifier
Error compiling Cython file:
------------------------------------------------------------
...
self._solver = s
cdef class InterpolantMC(__AbstractProver):
def __cinit__(self, Property p, SmtSolver s, SmtSolver interp):
self.cp = new c_InterpolantMC(p.cp[0], s.css, interp.css)
^
------------------------------------------------------------
/home/xxx/pono/python/pono_imp.pxi:425:22: new operator can only be applied to a C++ class
Error compiling Cython file:
------------------------------------------------------------
...
cdef class BTOR2Encoder:
cdef c_BTOR2Encoder * cbe
def __cinit__(self, str filename, __AbstractTransitionSystem ts):
self.cbe = new c_BTOR2Encoder(filename.encode(), dref(ts.cts))
^
------------------------------------------------------------
/home/xxx/pono/python/pono_imp.pxi:432:23: 'c_BTOR2Encoder' is not a type identifier
Error compiling Cython file:
------------------------------------------------------------
...
cdef class BTOR2Encoder:
cdef c_BTOR2Encoder * cbe
def __cinit__(self, str filename, __AbstractTransitionSystem ts):
self.cbe = new c_BTOR2Encoder(filename.encode(), dref(ts.cts))
^
------------------------------------------------------------
/home/xxx/pono/python/pono_imp.pxi:432:23: new operator can only be applied to a C++ class
Error compiling Cython file:
------------------------------------------------------------
...
raise ValueError("CoreIR encoder takes a pycoreir Context or a filename but got {}".format(mod))
def set_global_logger_verbosity(int v):
c_set_global_logger_verbosity(v)
^
------------------------------------------------------------
/home/xxx/pono/python/pono_imp.pxi:450:4: 'c_set_global_logger_verbosity' is not a constant, variable or function identifier
Error compiling Cython file:
------------------------------------------------------------
...
c_set_global_logger_verbosity(v)
def get_free_symbols(Term term):
cdef c_UnorderedTermSet out_symbols
c_get_free_symbols(term.ct, out_symbols)
^
------------------------------------------------------------
/home/xxx/pono/python/pono_imp.pxi:455:4: 'c_get_free_symbols' is not a constant, variable or function identifier
Error compiling Cython file:
------------------------------------------------------------
...
c_set_global_logger_verbosity(v)
def get_free_symbols(Term term):
cdef c_UnorderedTermSet out_symbols
c_get_free_symbols(term.ct, out_symbols)
^
------------------------------------------------------------
/home/xxx/pono/python/pono_imp.pxi:455:27: Cannot convert 'c_Term' to Python object
Error compiling Cython file:
------------------------------------------------------------
...
c_set_global_logger_verbosity(v)
def get_free_symbols(Term term):
cdef c_UnorderedTermSet out_symbols
c_get_free_symbols(term.ct, out_symbols)
^
------------------------------------------------------------
/home/xxx/pono/python/pono_imp.pxi:455:32: Cannot convert 'c_UnorderedTermSet' to Python object
make[2]: *** [python/CMakeFiles/pono.dir/build.make:94: python/pono.cxx] Error 1
make[2]: *** Deleting file 'python/pono.cxx'
make[1]: *** [CMakeFiles/Makefile2:294: python/CMakeFiles/pono.dir/all] Error 2
make: *** [Makefile:160: all] Error 2
Implement Cone of Influence reduction
Clean up array axiom enumeration
See comments on #69 for files refiners/axiom_enumerator.h and refiners/array_axiom_enumerator.h for more info.
- Return consecutive and nonconsecutive axioms as const references
- Pass axiom sets by reference to
index_axiomsandnon_index_axioms - Populate a new vector with axioms after reducing (this should be discussed but I think it's the only way to do it while using references to the axiom sets)
Improve interface with original TS
Handling multiple solvers is still ugly. In particular, one area this shows up is when the original transition system is different than the solver used in the engine. This is currently fairly ugly and inefficient. Additionally, it's easy to forget to set the original TS in some edge cases. For example, #255 included a fix for IC3IA where the original TS was lost. This is because it passes a fresh TS as the "main" one because that is the abstraction that other members needed access to right away (e.g. the abstractor classes) for modifying it. But then the orig_ts_ was not set correctly so we had to manually do that. But there's no infrastructure for ensuring that happens properly.
Implement Lazy Abstraction: Visible variables for FTS
Link error when building in github actions environment
Here's an example log: https://github.com/leonardt/fault/runs/1311361414?check_suite_focus=true
Since the undefined references involved string methods, I thought it might be related to -D_GLIBCXX_USE_CXX11_ABI=0. However from what I can tell, the coreir release being used is built on travis with gcc-7 without setting that define, and when I forced gcc-8 on github actions, still got the same error. One thing I haven't tried is building pono with -D_GLIBCXX_USE_CXX11_ABI=0, but given the next finding detailed below, I didn't pursue this.
What's even more confusing: building pono-lib works (linking coreir), but building the pono executable (which links pono-lib) fails with the linker errors, so that makes me think it's not related to the string ABI problems. I poked around and still couldn't seem to resolve the issue. This process seems to work fine on the pono travis environment, as well as my local macos environment, so I'm guessing it's something different about the github environment. I haven't been able to figure out what might be the cause though.
I did find that it seems that using target_sources (https://github.com/upscale-project/pono/blob/master/CMakeLists.txt#L167) causes the coreir_encoder.cpp file to be rebuilt for the executable. However, even when I changed the cmake logic to just use a SOURCES variable (https://github.com/upscale-project/pono/blob/7777658cbf349892341906ccb8716ab2117eef35/CMakeLists.txt#L157) to avoid the recompilation, I still got linker errors related to coreir (here's an example log: https://github.com/leonardt/fault/runs/1311285582?check_suite_focus=true). (again this recompilation doesn't seem to be problematic for pono travis or my local env)
FWIW: I managed to unblock myself by just building pono-lib since that's actually all I need for my flow, so I don't think this should be high priority until someone else comes along that is blocked by this issue. But I figured it's worth documenting so if it does come up again we have somewhere to start.
Here are the relevant error messages so it may be easier to find this note.
CMakeFiles/pono-bin.dir/frontends/coreir_encoder.cpp.o: In function `pono::CoreIREncoder::read_coreir_file(CoreIR::Context*, std::__cxx11::basic_string<char, std::char_traits<char>, std::allocator<char> >)':
coreir_encoder.cpp:(.text+0x54c): undefined reference to `CoreIR::loadFromFile(CoreIR::Context*, std::__cxx11::basic_string<char, std::char_traits<char>, std::allocator<char> >, CoreIR::Module**)'
CMakeFiles/pono-bin.dir/build.make:125: recipe for target 'pono' failed
CMakeFiles/pono-bin.dir/frontends/coreir_encoder.cpp.o: In function `pono::CoreIREncoder::process_instance(CoreIR::Instance*)':
CMakeFiles/Makefile2:277: recipe for target 'CMakeFiles/pono-bin.dir/all' failed
coreir_encoder.cpp:(.text+0x87d): undefined reference to `CoreIR::Instance::sel(std::__cxx11::basic_string<char, std::char_traits<char>, std::allocator<char> > const&)'
coreir_encoder.cpp:(.text+0x8c3): undefined reference to `CoreIR::Instance::sel(std::__cxx11::basic_string<char, std::char_traits<char>, std::allocator<char> > const&)'
coreir_encoder.cpp:(.text+0xa33): undefined reference to `CoreIR::Instance::sel(std::__cxx11::basic_string<char, std::char_traits<char>, std::allocator<char> > const&)'
coreir_encoder.cpp:(.text+0xceb): undefined reference to `CoreIR::Instance::sel(std::__cxx11::basic_string<char, std::char_traits<char>, std::allocator<char> > const&)'
coreir_encoder.cpp:(.text+0xd51): undefined reference to `CoreIR::Instance::sel(std::__cxx11::basic_string<char, std::char_traits<char>, std::allocator<char> > const&)'
CMakeFiles/pono-bin.dir/frontends/coreir_encoder.cpp.o:coreir_encoder.cpp:(.text+0xdbb): more undefined references to `CoreIR::Instance::sel(std::__cxx11::basic_string<char, std::char_traits<char>, std::allocator<char> > const&)' follow
CMakeFiles/pono-bin.dir/frontends/coreir_encoder.cpp.o: In function `pono::CoreIREncoder::wire_connection(std::pair<CoreIR::Wireable*, CoreIR::Wireable*>)':
coreir_encoder.cpp:(.text+0x2606): undefined reference to `CoreIR::isNumber(std::__cxx11::basic_string<char, std::char_traits<char>, std::allocator<char> >)'
coreir_encoder.cpp:(.text+0x2819): undefined reference to `CoreIR::isNumber(std::__cxx11::basic_string<char, std::char_traits<char>, std::allocator<char> >)'
CMakeFiles/pono-bin.dir/frontends/coreir_encoder.cpp.o: In function `pono::CoreIREncoder::process_state_element(CoreIR::Instance*)':
coreir_encoder.cpp:(.text+0x30d7): undefined reference to `CoreIR::Instance::sel(std::__cxx11::basic_string<char, std::char_traits<char>, std::allocator<char> > const&)'
coreir_encoder.cpp:(.text+0x3143): undefined reference to `CoreIR::Instance::sel(std::__cxx11::basic_string<char, std::char_traits<char>, std::allocator<char> > const&)'
coreir_encoder.cpp:(.text+0x348d): undefined reference to `CoreIR::Instance::sel(std::__cxx11::basic_string<char, std::char_traits<char>, std::allocator<char> > const&)'
coreir_encoder.cpp:(.text+0x34f3): undefined reference to `CoreIR::Instance::sel(std::__cxx11::basic_string<char, std::char_traits<char>, std::allocator<char> > const&)'
coreir_encoder.cpp:(.text+0x3565): undefined reference to `CoreIR::Instance::sel(std::__cxx11::basic_string<char, std::char_traits<char>, std::allocator<char> > const&)'
CMakeFiles/pono-bin.dir/frontends/coreir_encoder.cpp.o:coreir_encoder.cpp:(.text+0x35c0): more undefined references to `CoreIR::Instance::sel(std::__cxx11::basic_string<char, std::char_traits<char>, std::allocator<char> > const&)' follow
CMakeFiles/pono-bin.dir/frontends/coreir_encoder.cpp.o: In function `pono::CoreIREncoder::encode()':
coreir_encoder.cpp:(.text+0x4a79): undefined reference to `CoreIR::Context::runPasses(std::vector<std::__cxx11::basic_string<char, std::char_traits<char>, std::allocator<char> >, std::allocator<std::__cxx11::basic_string<char, std::char_traits<char>, std::allocator<char> > > >, std::vector<std::__cxx11::basic_string<char, std::char_traits<char>, std::allocator<char> >, std::allocator<std::__cxx11::basic_string<char, std::char_traits<char>, std::allocator<char> > > >)'
coreir_encoder.cpp:(.text+0x573c): undefined reference to `CoreIR::isNumber(std::__cxx11::basic_string<char, std::char_traits<char>, std::allocator<char> >)'
coreir_encoder.cpp:(.text+0x6185): undefined reference to `CoreIR::isNumber(std::__cxx11::basic_string<char, std::char_traits<char>, std::allocator<char> >)'
CMakeFiles/pono-bin.dir/frontends/coreir_encoder.cpp.o: In function `CoreIR::Module::getGenArgs[abi:cxx11]()':
coreir_encoder.cpp:(.text._ZN6CoreIR6Module10getGenArgsB5cxx11Ev[_ZN6CoreIR6Module10getGenArgsB5cxx11Ev]+0x127): undefined reference to `CoreIR::GlobalValue::getRefName[abi:cxx11]() const'
collect2: error: ld returned 1 exit status
libpono.so: undefined reference to `CoreIR::GlobalValue::getRefName[abi:cxx11]() const'
libpono.so: undefined reference to `CoreIR::Context::runPasses(std::vector<std::__cxx11::basic_string<char, std::char_traits<char>, std::allocator<char> >, std::allocator<std::__cxx11::basic_string<char, std::char_traits<char>, std::allocator<char> > > >, std::vector<std::__cxx11::basic_string<char, std::char_traits<char>, std::allocator<char> >, std::allocator<std::__cxx11::basic_string<char, std::char_traits<char>, std::allocator<char> > > >)'
CMakeFiles/pono-bin.dir/build.make:110: recipe for target 'pono' failed
libpono.so: undefined reference to `CoreIR::loadFromFile(CoreIR::Context*, std::__cxx11::basic_string<char, std::char_traits<char>, std::allocator<char> >, CoreIR::Module**)'
CMakeFiles/Makefile2:277: recipe for target 'CMakeFiles/pono-bin.dir/all' failed
libpono.so: undefined reference to `CoreIR::Instance::sel(std::__cxx11::basic_string<char, std::char_traits<char>, std::allocator<char> > const&)'
libpono.so: undefined reference to `CoreIR::isNumber(std::__cxx11::basic_string<char, std::char_traits<char>, std::allocator<char> >)'
Crash when extracting counterexample trace
Attached are the Verilog and Btor2 that will trigger crash (segmentation fault) when extracting counter-example trace in Prover::witness at Term r = solver_->get_value(vi);.
I think it is on m1.l15.mshr.ld_homeid (which is an array) at time 0. I'm sorry but I don't think I'm knowledgeable enough to tell what exactly causes the problem.
Thanks!
Improve infrastructure for transferring between solvers
It is often a headache to maintain formulas over multiple solvers. This can be seen with complicated code in some areas, for example:
- https://github.com/upscale-project/pono/blob/a2d993cc8c3a948150586ce014066f479045a74a/engines/ic3ia.cpp#L156
- This case occurs with IC3IA because the UF abstraction symbols already exist in the solver but are not in the TermTranslator's cache so they can't be looked up https://github.com/upscale-project/pono/blob/a2d993cc8c3a948150586ce014066f479045a74a/engines/ceg_prophecy_arrays.cpp#L165
We need a better way to manage multiple solvers.
Python bindings should use `-undefined dynamic_lookup` when `Py_ENABLE_SHARED` is 0
Walked through the README steps and ran into a seg fault trying to run the test suite:
~/repos/pono master*
base ❯ pytest ./tests
===================================================================== test session starts ======================================================================
platform darwin -- Python 3.8.3, pytest-6.0.0, py-1.9.0, pluggy-0.13.1
rootdir: /Users/lenny/repos/pono
plugins: pycodestyle-2.2.0
collecting ... Fatal Python error: Segmentation fault
Current thread 0x000000011de01dc0 (most recent call first):
File "<frozen importlib._bootstrap>", line 219 in _call_with_frames_removed
File "<frozen importlib._bootstrap_external>", line 1101 in create_module
File "<frozen importlib._bootstrap>", line 556 in module_from_spec
File "<frozen importlib._bootstrap>", line 657 in _load_unlocked
File "<frozen importlib._bootstrap>", line 975 in _find_and_load_unlocked
File "<frozen importlib._bootstrap>", line 991 in _find_and_load
File "/Users/lenny/repos/pono/tests/python/test_encoders.py", line 2 in <module>
File "/Users/lenny/miniconda3/lib/python3.8/site-packages/_pytest/assertion/rewrite.py", line 170 in exec_module
File "<frozen importlib._bootstrap>", line 671 in _load_unlocked
File "<frozen importlib._bootstrap>", line 975 in _find_and_load_unlocked
File "<frozen importlib._bootstrap>", line 991 in _find_and_load
File "<frozen importlib._bootstrap>", line 1014 in _gcd_import
File "/Users/lenny/miniconda3/lib/python3.8/importlib/__init__.py", line 127 in import_module
File "/Users/lenny/miniconda3/lib/python3.8/site-packages/_pytest/pathlib.py", line 520 in import_path
File "/Users/lenny/miniconda3/lib/python3.8/site-packages/_pytest/python.py", line 552 in _importtestmodule
File "/Users/lenny/miniconda3/lib/python3.8/site-packages/_pytest/python.py", line 484 in _getobj
File "/Users/lenny/miniconda3/lib/python3.8/site-packages/_pytest/python.py", line 288 in obj
File "/Users/lenny/miniconda3/lib/python3.8/site-packages/_pytest/python.py", line 500 in _inject_setup_module_fixture
File "/Users/lenny/miniconda3/lib/python3.8/site-packages/_pytest/python.py", line 487 in collect
File "/Users/lenny/miniconda3/lib/python3.8/site-packages/_pytest/runner.py", line 324 in <lambda>
File "/Users/lenny/miniconda3/lib/python3.8/site-packages/_pytest/runner.py", line 294 in from_call
File "/Users/lenny/miniconda3/lib/python3.8/site-packages/_pytest/runner.py", line 324 in pytest_make_collect_report
File "/Users/lenny/miniconda3/lib/python3.8/site-packages/pluggy/callers.py", line 187 in _multicall
File "/Users/lenny/miniconda3/lib/python3.8/site-packages/pluggy/manager.py", line 84 in <lambda>
File "/Users/lenny/miniconda3/lib/python3.8/site-packages/pluggy/manager.py", line 93 in _hookexec
File "/Users/lenny/miniconda3/lib/python3.8/site-packages/pluggy/hooks.py", line 286 in __call__
File "/Users/lenny/miniconda3/lib/python3.8/site-packages/_pytest/runner.py", line 441 in collect_one_node
File "/Users/lenny/miniconda3/lib/python3.8/site-packages/_pytest/main.py", line 768 in genitems
File "/Users/lenny/miniconda3/lib/python3.8/site-packages/_pytest/main.py", line 568 in _perform_collect
File "/Users/lenny/miniconda3/lib/python3.8/site-packages/_pytest/main.py", line 516 in perform_collect
File "/Users/lenny/miniconda3/lib/python3.8/site-packages/_pytest/main.py", line 306 in pytest_collection
File "/Users/lenny/miniconda3/lib/python3.8/site-packages/pluggy/callers.py", line 187 in _multicall
File "/Users/lenny/miniconda3/lib/python3.8/site-packages/pluggy/manager.py", line 84 in <lambda>
File "/Users/lenny/miniconda3/lib/python3.8/site-packages/pluggy/manager.py", line 93 in _hookexec
File "/Users/lenny/miniconda3/lib/python3.8/site-packages/pluggy/hooks.py", line 286 in __call__
File "/Users/lenny/miniconda3/lib/python3.8/site-packages/_pytest/main.py", line 295 in _main
File "/Users/lenny/miniconda3/lib/python3.8/site-packages/_pytest/main.py", line 240 in wrap_session
File "/Users/lenny/miniconda3/lib/python3.8/site-packages/_pytest/main.py", line 289 in pytest_cmdline_main
File "/Users/lenny/miniconda3/lib/python3.8/site-packages/pluggy/callers.py", line 187 in _multicall
File "/Users/lenny/miniconda3/lib/python3.8/site-packages/pluggy/manager.py", line 84 in <lambda>
File "/Users/lenny/miniconda3/lib/python3.8/site-packages/pluggy/manager.py", line 93 in _hookexec
File "/Users/lenny/miniconda3/lib/python3.8/site-packages/pluggy/hooks.py", line 286 in __call__
File "/Users/lenny/miniconda3/lib/python3.8/site-packages/_pytest/config/__init__.py", line 157 in main
File "/Users/lenny/miniconda3/lib/python3.8/site-packages/_pytest/config/__init__.py", line 180 in console_main
File "/Users/lenny/miniconda3/bin/pytest", line 8 in <module>
zsh: segmentation fault pytest ./tests
I traced the issue to the import pono step, here's a backtrace produced by lldb:
~/repos/pono master*
base ❯ lldb -- ~/miniconda3/bin/python -c "import pono"
(lldb) target create "/Users/lenny/miniconda3/bin/python"
Current executable set to '/Users/lenny/miniconda3/bin/python' (x86_64).
(lldb) settings set -- target.run-args "-c" "import pono"
(lldb) r
Process 98745 launched: '/Users/lenny/miniconda3/bin/python' (x86_64)
Process 98745 stopped
* thread #1, queue = 'com.apple.main-thread', stop reason = EXC_BAD_ACCESS (code=1, address=0x8)
frame #0: 0x0000000104613797 libpython3.8.dylib`PyType_Ready + 455
libpython3.8.dylib`PyType_Ready:
-> 0x104613797 <+455>: movq 0x8(%rcx), %rdx
0x10461379b <+459>: movq %rax, (%rdx)
0x10461379e <+462>: movq -0x8(%rbx), %rsi
0x1046137a2 <+466>: andl $0x3, %esi
Target 0: (python) stopped.
(lldb) bt
* thread #1, queue = 'com.apple.main-thread', stop reason = EXC_BAD_ACCESS (code=1, address=0x8)
* frame #0: 0x0000000104613797 libpython3.8.dylib`PyType_Ready + 455
frame #1: 0x000000010461368f libpython3.8.dylib`PyType_Ready + 191
frame #2: 0x00000001045f6e99 libpython3.8.dylib`PyModuleDef_Init + 25
frame #3: 0x00000001001a7645 python`_PyImport_LoadDynamicModuleWithSpec + 565
frame #4: 0x00000001001a64e5 python`_imp_create_dynamic + 181
frame #5: 0x000000010008aea4 python`cfunction_vectorcall_FASTCALL + 84
frame #6: 0x000000010002dbd9 python`PyVectorcall_Call + 121
frame #7: 0x0000000100164d6f python`_PyEval_EvalFrameDefault + 47711
frame #8: 0x000000010015752d python`_PyEval_EvalCodeWithName + 557
frame #9: 0x000000010002e8ca python`_PyFunction_Vectorcall + 426
frame #10: 0x000000010016430b python`_PyEval_EvalFrameDefault + 45051
frame #11: 0x000000010002e818 python`_PyFunction_Vectorcall + 248
frame #12: 0x0000000100164216 python`_PyEval_EvalFrameDefault + 44806
frame #13: 0x000000010002e818 python`_PyFunction_Vectorcall + 248
frame #14: 0x000000010016469b python`_PyEval_EvalFrameDefault + 45963
frame #15: 0x000000010002e818 python`_PyFunction_Vectorcall + 248
frame #16: 0x000000010016469b python`_PyEval_EvalFrameDefault + 45963
frame #17: 0x000000010002e818 python`_PyFunction_Vectorcall + 248
frame #18: 0x000000010016469b python`_PyEval_EvalFrameDefault + 45963
frame #19: 0x000000010002e818 python`_PyFunction_Vectorcall + 248
frame #20: 0x0000000100030686 python`object_vacall + 374
frame #21: 0x000000010003090d python`_PyObject_CallMethodIdObjArgs + 237
frame #22: 0x00000001001a060e python`PyImport_ImportModuleLevelObject + 1342
frame #23: 0x00000001001618df python`_PyEval_EvalFrameDefault + 34255
frame #24: 0x000000010015752d python`_PyEval_EvalCodeWithName + 557
frame #25: 0x00000001001d2a03 python`PyRun_StringFlags + 259
frame #26: 0x00000001001d2852 python`PyRun_SimpleStringFlags + 82
frame #27: 0x00000001001f7ba6 python`pymain_run_command + 134
frame #28: 0x00000001001f6bdd python`pymain_run_python + 477
frame #29: 0x00000001001f69a5 python`Py_RunMain + 37
frame #30: 0x00000001001f7f41 python`pymain_main + 49
frame #31: 0x0000000100000d68 python`main + 56
frame #32: 0x00007fff67ed7cc9 libdyld.dylib`start + 1
(lldb)
Have you seen anything like this before? I'm going to try rebuilding from scratch to make sure I didn't mess up a step.
Constraint Handling
Hi I have a question about the part that handles Btor2 constraints.
Suppose that the expression of the constraint is C.
What the code does is: if C does not contain input, then C(V) and C(V') will be added to the transition relation.
But if C contains input, only C(V) will be added to the transition relation.
But why is that (I mean why there is such a difference)?
Furthermore, what if C syntactically contains some input variable, but semantically that input variable is reducible (I know that Boolector will do some reduction that may be able to remove it, but I guess there might also be cases where Boolector is not smart enough to do so). Does it matter? Would anything bad happen in this case?
step function of the interpolantion engine is not aligned with other engines
Don't declare states/inputs up front
There are often scenarios where an input needs to be "promoted" to a state variable based on some added constraints (important for soundness!). This is much easier to do if they are not declared beforehand, but instead marked as states later.
Look into performance issues with large unrolls
Cosa2 takes 4m to unroll to bound 26,000 on my desktop, and btormc takes only 9s to unroll and solve.
Special unroller for functional unrolling
Segfault in CVC4 when copying default transition system
This bug could be in smt-switch or CVC4 as well, because this doesn't occur when I tried switching the default solver to MathSAT. It's unclear at this point where exactly the problem is.
support for Arithmetic Theories
Handle state variables without next-function as inputs
Issue refers to BTOR2 inputs and Pono master 5b6af14.
Excerpt from the BTOR2 paper (https://link.springer.com/content/pdf/10.1007%2F978-3-319-96145-3_32.pdf):
"A state variable without associated next function is treated as a primary input, i.e., it has the same behaviour as inputs defined via keyword input."
Pono properly handles inputs that are explicitly declared using the keyword input. Such inputs are added to the set inputvars_ of a transition system.
However, state variables declared using the keyword state and for which no next-function is given are added to the set statevars_ of a transition system although according to the BTOR2 standard they should appear in inputvars_.
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.