search

meelgroup / bosphorus

Bosphorus, ANF simplifier and solver, and ANF-to-CNF converter
Other
67 stars 18 forks source link

ANF projection set parsing skips file after first comment #44

Closed tanyongkiam closed 1 year ago

tanyongkiam commented 1 year ago

Upon reading a regular comment line c foo ..., the following lines in the projection set parser appear to break entirely out of the ANF parsing loop (and ignore the rest of the input file). I guess they should continue instead of break.

https://github.com/meelgroup/bosphorus/blob/master/src/anf.cpp#L131 https://github.com/meelgroup/bosphorus/blob/master/src/anf.cpp#L133 https://github.com/meelgroup/bosphorus/blob/master/src/anf.cpp#L135

Example file:

x(0)
x(2)
c foo
x(1)

Bosphorus with --allsol gives:

...
s ANF-SATISFIABLE
v x(0) x(1) x(2) 
c Solution found is correct.
s ANF-SATISFIABLE
v x(0) 1+x(1) x(2) 
c Solution found is correct.
s ANF-UNSATISFIABLE
c Number of solutions found: 2
msoos commented 1 year ago

Oh wow, you are right! I'm so sorry. I added exactly your fix: bd1b643560c0ebe0af5deb28403e158b133be529 Thanks again.

I should have some test cases :S Maybe I should have some tests.... it takes quite a bit of time to set up. I'm adding an issue related to missing end-to-end tests.